Termination w.r.t. Q proof of /tmp/tmpAVK31i/ExAppendixB_AEL03

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

2NDSPOS(X1, active(X2)) → 2NDSPOS(X1, X2)
ACTIVE(times(s(X), Y)) → MARK(plus(Y, times(X, Y)))
TIMES(X1, active(X2)) → TIMES(X1, X2)
MARK(2ndspos(X1, X2)) → MARK(X2)
CONS(X1, mark(X2)) → CONS(X1, X2)
POSRECIP(active(X)) → POSRECIP(X)
MARK(2ndspos(X1, X2)) → ACTIVE(2ndspos(mark(X1), mark(X2)))
CONS2(mark(X1), X2) → CONS2(X1, X2)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
ACTIVE(pi(X)) → FROM(0)
TIMES(mark(X1), X2) → TIMES(X1, X2)
MARK(cons2(X1, X2)) → CONS2(X1, mark(X2))
ACTIVE(2ndsneg(s(N), cons(X, Z))) → CONS2(X, Z)
ACTIVE(plus(0, Y)) → MARK(Y)
MARK(2ndspos(X1, X2)) → 2NDSPOS(mark(X1), mark(X2))
NEGRECIP(mark(X)) → NEGRECIP(X)
MARK(2ndsneg(X1, X2)) → ACTIVE(2ndsneg(mark(X1), mark(X2)))
2NDSNEG(active(X1), X2) → 2NDSNEG(X1, X2)
MARK(rnil) → ACTIVE(rnil)
ACTIVE(square(X)) → TIMES(X, X)
PI(active(X)) → PI(X)
2NDSPOS(X1, mark(X2)) → 2NDSPOS(X1, X2)
2NDSPOS(active(X1), X2) → 2NDSPOS(X1, X2)
2NDSNEG(mark(X1), X2) → 2NDSNEG(X1, X2)
ACTIVE(2ndspos(s(N), cons(X, Z))) → CONS2(X, Z)
MARK(cons2(X1, X2)) → MARK(X2)
ACTIVE(square(X)) → MARK(times(X, X))
CONS(mark(X1), X2) → CONS(X1, X2)
MARK(2ndspos(X1, X2)) → MARK(X1)
MARK(s(X)) → MARK(X)
MARK(from(X)) → FROM(mark(X))
ACTIVE(2ndspos(s(N), cons(X, Z))) → 2NDSPOS(s(N), cons2(X, Z))
PLUS(mark(X1), X2) → PLUS(X1, X2)
MARK(pi(X)) → MARK(X)
MARK(plus(X1, X2)) → MARK(X2)
CONS(X1, active(X2)) → CONS(X1, X2)
ACTIVE(2ndspos(s(N), cons2(X, cons(Y, Z)))) → RCONS(posrecip(Y), 2ndsneg(N, Z))
MARK(s(X)) → ACTIVE(s(mark(X)))
PLUS(X1, mark(X2)) → PLUS(X1, X2)
MARK(2ndsneg(X1, X2)) → MARK(X2)
PLUS(X1, active(X2)) → PLUS(X1, X2)
ACTIVE(pi(X)) → 2NDSPOS(X, from(0))
2NDSNEG(X1, active(X2)) → 2NDSNEG(X1, X2)
S(mark(X)) → S(X)
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
ACTIVE(2ndspos(s(N), cons2(X, cons(Y, Z)))) → MARK(rcons(posrecip(Y), 2ndsneg(N, Z)))
2NDSPOS(mark(X1), X2) → 2NDSPOS(X1, X2)
MARK(plus(X1, X2)) → MARK(X1)
MARK(times(X1, X2)) → ACTIVE(times(mark(X1), mark(X2)))
ACTIVE(2ndspos(0, Z)) → MARK(rnil)
MARK(square(X)) → ACTIVE(square(mark(X)))
ACTIVE(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → RCONS(negrecip(Y), 2ndspos(N, Z))
ACTIVE(plus(s(X), Y)) → S(plus(X, Y))
ACTIVE(from(X)) → S(X)
ACTIVE(2ndspos(s(N), cons2(X, cons(Y, Z)))) → POSRECIP(Y)
SQUARE(active(X)) → SQUARE(X)
ACTIVE(times(0, Y)) → MARK(0)
ACTIVE(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → MARK(rcons(negrecip(Y), 2ndspos(N, Z)))
FROM(mark(X)) → FROM(X)
RCONS(active(X1), X2) → RCONS(X1, X2)
MARK(square(X)) → SQUARE(mark(X))
MARK(cons(X1, X2)) → MARK(X1)
FROM(active(X)) → FROM(X)
CONS2(X1, mark(X2)) → CONS2(X1, X2)
ACTIVE(times(s(X), Y)) → TIMES(X, Y)
ACTIVE(2ndsneg(s(N), cons(X, Z))) → MARK(2ndsneg(s(N), cons2(X, Z)))
ACTIVE(2ndsneg(s(N), cons(X, Z))) → 2NDSNEG(s(N), cons2(X, Z))
ACTIVE(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → NEGRECIP(Y)
MARK(posrecip(X)) → POSRECIP(mark(X))
MARK(times(X1, X2)) → MARK(X2)
ACTIVE(2ndspos(s(N), cons(X, Z))) → MARK(2ndspos(s(N), cons2(X, Z)))
MARK(posrecip(X)) → ACTIVE(posrecip(mark(X)))
PI(mark(X)) → PI(X)
ACTIVE(plus(s(X), Y)) → PLUS(X, Y)
MARK(plus(X1, X2)) → ACTIVE(plus(mark(X1), mark(X2)))
MARK(2ndsneg(X1, X2)) → MARK(X1)
2NDSNEG(X1, mark(X2)) → 2NDSNEG(X1, X2)
SQUARE(mark(X)) → SQUARE(X)
ACTIVE(2ndsneg(0, Z)) → MARK(rnil)
MARK(rcons(X1, X2)) → MARK(X1)
S(active(X)) → S(X)
MARK(cons(X1, X2)) → CONS(mark(X1), X2)
TIMES(active(X1), X2) → TIMES(X1, X2)
RCONS(X1, mark(X2)) → RCONS(X1, X2)
MARK(times(X1, X2)) → TIMES(mark(X1), mark(X2))
MARK(square(X)) → MARK(X)
MARK(cons2(X1, X2)) → ACTIVE(cons2(X1, mark(X2)))
CONS(active(X1), X2) → CONS(X1, X2)
CONS2(X1, active(X2)) → CONS2(X1, X2)
MARK(rcons(X1, X2)) → ACTIVE(rcons(mark(X1), mark(X2)))
MARK(rcons(X1, X2)) → MARK(X2)
ACTIVE(from(X)) → FROM(s(X))
ACTIVE(times(s(X), Y)) → PLUS(Y, times(X, Y))
RCONS(X1, active(X2)) → RCONS(X1, X2)
MARK(rcons(X1, X2)) → RCONS(mark(X1), mark(X2))
MARK(negrecip(X)) → ACTIVE(negrecip(mark(X)))
PLUS(active(X1), X2) → PLUS(X1, X2)
MARK(times(X1, X2)) → MARK(X1)
ACTIVE(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → 2NDSPOS(N, Z)
MARK(pi(X)) → PI(mark(X))
MARK(negrecip(X)) → MARK(X)
RCONS(mark(X1), X2) → RCONS(X1, X2)
MARK(posrecip(X)) → MARK(X)
ACTIVE(2ndspos(s(N), cons2(X, cons(Y, Z)))) → 2NDSNEG(N, Z)
ACTIVE(pi(X)) → MARK(2ndspos(X, from(0)))
MARK(s(X)) → S(mark(X))
MARK(from(X)) → MARK(X)
NEGRECIP(active(X)) → NEGRECIP(X)
POSRECIP(mark(X)) → POSRECIP(X)
MARK(2ndsneg(X1, X2)) → 2NDSNEG(mark(X1), mark(X2))
MARK(from(X)) → ACTIVE(from(mark(X)))
MARK(0) → ACTIVE(0)
MARK(plus(X1, X2)) → PLUS(mark(X1), mark(X2))
MARK(negrecip(X)) → NEGRECIP(mark(X))
TIMES(X1, mark(X2)) → TIMES(X1, X2)
ACTIVE(plus(s(X), Y)) → MARK(s(plus(X, Y)))
MARK(pi(X)) → ACTIVE(pi(mark(X)))
ACTIVE(from(X)) → CONS(X, from(s(X)))
CONS2(active(X1), X2) → CONS2(X1, X2)

The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

2NDSPOS(X1, active(X2)) → 2NDSPOS(X1, X2)
ACTIVE(times(s(X), Y)) → MARK(plus(Y, times(X, Y)))
TIMES(X1, active(X2)) → TIMES(X1, X2)
MARK(2ndspos(X1, X2)) → MARK(X2)
CONS(X1, mark(X2)) → CONS(X1, X2)
POSRECIP(active(X)) → POSRECIP(X)
MARK(2ndspos(X1, X2)) → ACTIVE(2ndspos(mark(X1), mark(X2)))
CONS2(mark(X1), X2) → CONS2(X1, X2)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
ACTIVE(pi(X)) → FROM(0)
TIMES(mark(X1), X2) → TIMES(X1, X2)
MARK(cons2(X1, X2)) → CONS2(X1, mark(X2))
ACTIVE(2ndsneg(s(N), cons(X, Z))) → CONS2(X, Z)
ACTIVE(plus(0, Y)) → MARK(Y)
MARK(2ndspos(X1, X2)) → 2NDSPOS(mark(X1), mark(X2))
NEGRECIP(mark(X)) → NEGRECIP(X)
MARK(2ndsneg(X1, X2)) → ACTIVE(2ndsneg(mark(X1), mark(X2)))
2NDSNEG(active(X1), X2) → 2NDSNEG(X1, X2)
MARK(rnil) → ACTIVE(rnil)
ACTIVE(square(X)) → TIMES(X, X)
PI(active(X)) → PI(X)
2NDSPOS(X1, mark(X2)) → 2NDSPOS(X1, X2)
2NDSPOS(active(X1), X2) → 2NDSPOS(X1, X2)
2NDSNEG(mark(X1), X2) → 2NDSNEG(X1, X2)
ACTIVE(2ndspos(s(N), cons(X, Z))) → CONS2(X, Z)
MARK(cons2(X1, X2)) → MARK(X2)
ACTIVE(square(X)) → MARK(times(X, X))
CONS(mark(X1), X2) → CONS(X1, X2)
MARK(2ndspos(X1, X2)) → MARK(X1)
MARK(s(X)) → MARK(X)
MARK(from(X)) → FROM(mark(X))
ACTIVE(2ndspos(s(N), cons(X, Z))) → 2NDSPOS(s(N), cons2(X, Z))
PLUS(mark(X1), X2) → PLUS(X1, X2)
MARK(pi(X)) → MARK(X)
MARK(plus(X1, X2)) → MARK(X2)
CONS(X1, active(X2)) → CONS(X1, X2)
ACTIVE(2ndspos(s(N), cons2(X, cons(Y, Z)))) → RCONS(posrecip(Y), 2ndsneg(N, Z))
MARK(s(X)) → ACTIVE(s(mark(X)))
PLUS(X1, mark(X2)) → PLUS(X1, X2)
MARK(2ndsneg(X1, X2)) → MARK(X2)
PLUS(X1, active(X2)) → PLUS(X1, X2)
ACTIVE(pi(X)) → 2NDSPOS(X, from(0))
2NDSNEG(X1, active(X2)) → 2NDSNEG(X1, X2)
S(mark(X)) → S(X)
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
ACTIVE(2ndspos(s(N), cons2(X, cons(Y, Z)))) → MARK(rcons(posrecip(Y), 2ndsneg(N, Z)))
2NDSPOS(mark(X1), X2) → 2NDSPOS(X1, X2)
MARK(plus(X1, X2)) → MARK(X1)
MARK(times(X1, X2)) → ACTIVE(times(mark(X1), mark(X2)))
ACTIVE(2ndspos(0, Z)) → MARK(rnil)
MARK(square(X)) → ACTIVE(square(mark(X)))
ACTIVE(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → RCONS(negrecip(Y), 2ndspos(N, Z))
ACTIVE(plus(s(X), Y)) → S(plus(X, Y))
ACTIVE(from(X)) → S(X)
ACTIVE(2ndspos(s(N), cons2(X, cons(Y, Z)))) → POSRECIP(Y)
SQUARE(active(X)) → SQUARE(X)
ACTIVE(times(0, Y)) → MARK(0)
ACTIVE(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → MARK(rcons(negrecip(Y), 2ndspos(N, Z)))
FROM(mark(X)) → FROM(X)
RCONS(active(X1), X2) → RCONS(X1, X2)
MARK(square(X)) → SQUARE(mark(X))
MARK(cons(X1, X2)) → MARK(X1)
FROM(active(X)) → FROM(X)
CONS2(X1, mark(X2)) → CONS2(X1, X2)
ACTIVE(times(s(X), Y)) → TIMES(X, Y)
ACTIVE(2ndsneg(s(N), cons(X, Z))) → MARK(2ndsneg(s(N), cons2(X, Z)))
ACTIVE(2ndsneg(s(N), cons(X, Z))) → 2NDSNEG(s(N), cons2(X, Z))
ACTIVE(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → NEGRECIP(Y)
MARK(posrecip(X)) → POSRECIP(mark(X))
MARK(times(X1, X2)) → MARK(X2)
ACTIVE(2ndspos(s(N), cons(X, Z))) → MARK(2ndspos(s(N), cons2(X, Z)))
MARK(posrecip(X)) → ACTIVE(posrecip(mark(X)))
PI(mark(X)) → PI(X)
ACTIVE(plus(s(X), Y)) → PLUS(X, Y)
MARK(plus(X1, X2)) → ACTIVE(plus(mark(X1), mark(X2)))
MARK(2ndsneg(X1, X2)) → MARK(X1)
2NDSNEG(X1, mark(X2)) → 2NDSNEG(X1, X2)
SQUARE(mark(X)) → SQUARE(X)
ACTIVE(2ndsneg(0, Z)) → MARK(rnil)
MARK(rcons(X1, X2)) → MARK(X1)
S(active(X)) → S(X)
MARK(cons(X1, X2)) → CONS(mark(X1), X2)
TIMES(active(X1), X2) → TIMES(X1, X2)
RCONS(X1, mark(X2)) → RCONS(X1, X2)
MARK(times(X1, X2)) → TIMES(mark(X1), mark(X2))
MARK(square(X)) → MARK(X)
MARK(cons2(X1, X2)) → ACTIVE(cons2(X1, mark(X2)))
CONS(active(X1), X2) → CONS(X1, X2)
CONS2(X1, active(X2)) → CONS2(X1, X2)
MARK(rcons(X1, X2)) → ACTIVE(rcons(mark(X1), mark(X2)))
MARK(rcons(X1, X2)) → MARK(X2)
ACTIVE(from(X)) → FROM(s(X))
ACTIVE(times(s(X), Y)) → PLUS(Y, times(X, Y))
RCONS(X1, active(X2)) → RCONS(X1, X2)
MARK(rcons(X1, X2)) → RCONS(mark(X1), mark(X2))
MARK(negrecip(X)) → ACTIVE(negrecip(mark(X)))
PLUS(active(X1), X2) → PLUS(X1, X2)
MARK(times(X1, X2)) → MARK(X1)
ACTIVE(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → 2NDSPOS(N, Z)
MARK(pi(X)) → PI(mark(X))
MARK(negrecip(X)) → MARK(X)
RCONS(mark(X1), X2) → RCONS(X1, X2)
MARK(posrecip(X)) → MARK(X)
ACTIVE(2ndspos(s(N), cons2(X, cons(Y, Z)))) → 2NDSNEG(N, Z)
ACTIVE(pi(X)) → MARK(2ndspos(X, from(0)))
MARK(s(X)) → S(mark(X))
MARK(from(X)) → MARK(X)
NEGRECIP(active(X)) → NEGRECIP(X)
POSRECIP(mark(X)) → POSRECIP(X)
MARK(2ndsneg(X1, X2)) → 2NDSNEG(mark(X1), mark(X2))
MARK(from(X)) → ACTIVE(from(mark(X)))
MARK(0) → ACTIVE(0)
MARK(plus(X1, X2)) → PLUS(mark(X1), mark(X2))
MARK(negrecip(X)) → NEGRECIP(mark(X))
TIMES(X1, mark(X2)) → TIMES(X1, X2)
ACTIVE(plus(s(X), Y)) → MARK(s(plus(X, Y)))
MARK(pi(X)) → ACTIVE(pi(mark(X)))
ACTIVE(from(X)) → CONS(X, from(s(X)))
CONS2(active(X1), X2) → CONS2(X1, X2)

The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 14 SCCs with 38 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SQUARE(mark(X)) → SQUARE(X)
SQUARE(active(X)) → SQUARE(X)

The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SQUARE(mark(X)) → SQUARE(X)
SQUARE(active(X)) → SQUARE(X)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

SQUARE(mark(X)) → SQUARE(X)
The graph contains the following edges 1 > 1
SQUARE(active(X)) → SQUARE(X)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

TIMES(active(X1), X2) → TIMES(X1, X2)
TIMES(X1, active(X2)) → TIMES(X1, X2)
TIMES(X1, mark(X2)) → TIMES(X1, X2)
TIMES(mark(X1), X2) → TIMES(X1, X2)

The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

TIMES(active(X1), X2) → TIMES(X1, X2)
TIMES(X1, active(X2)) → TIMES(X1, X2)
TIMES(X1, mark(X2)) → TIMES(X1, X2)
TIMES(mark(X1), X2) → TIMES(X1, X2)

From the DPs we obtained the following set of size-change graphs:

TIMES(active(X1), X2) → TIMES(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2
TIMES(X1, active(X2)) → TIMES(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2
TIMES(X1, mark(X2)) → TIMES(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2
TIMES(mark(X1), X2) → TIMES(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PLUS(active(X1), X2) → PLUS(X1, X2)
PLUS(mark(X1), X2) → PLUS(X1, X2)
PLUS(X1, mark(X2)) → PLUS(X1, X2)
PLUS(X1, active(X2)) → PLUS(X1, X2)

The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PLUS(active(X1), X2) → PLUS(X1, X2)
PLUS(mark(X1), X2) → PLUS(X1, X2)
PLUS(X1, mark(X2)) → PLUS(X1, X2)
PLUS(X1, active(X2)) → PLUS(X1, X2)

From the DPs we obtained the following set of size-change graphs:

PLUS(active(X1), X2) → PLUS(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2
PLUS(mark(X1), X2) → PLUS(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2
PLUS(X1, mark(X2)) → PLUS(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2
PLUS(X1, active(X2)) → PLUS(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PI(active(X)) → PI(X)
PI(mark(X)) → PI(X)

The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

PI(active(X)) → PI(X)
PI(mark(X)) → PI(X)

From the DPs we obtained the following set of size-change graphs:

PI(active(X)) → PI(X)
The graph contains the following edges 1 > 1
PI(mark(X)) → PI(X)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

NEGRECIP(active(X)) → NEGRECIP(X)
NEGRECIP(mark(X)) → NEGRECIP(X)

The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

NEGRECIP(active(X)) → NEGRECIP(X)
NEGRECIP(mark(X)) → NEGRECIP(X)

From the DPs we obtained the following set of size-change graphs:

NEGRECIP(active(X)) → NEGRECIP(X)
The graph contains the following edges 1 > 1
NEGRECIP(mark(X)) → NEGRECIP(X)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

2NDSNEG(X1, active(X2)) → 2NDSNEG(X1, X2)
2NDSNEG(mark(X1), X2) → 2NDSNEG(X1, X2)
2NDSNEG(X1, mark(X2)) → 2NDSNEG(X1, X2)
2NDSNEG(active(X1), X2) → 2NDSNEG(X1, X2)

The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

2NDSNEG(X1, active(X2)) → 2NDSNEG(X1, X2)
2NDSNEG(mark(X1), X2) → 2NDSNEG(X1, X2)
2NDSNEG(X1, mark(X2)) → 2NDSNEG(X1, X2)
2NDSNEG(active(X1), X2) → 2NDSNEG(X1, X2)

From the DPs we obtained the following set of size-change graphs:

2NDSNEG(X1, active(X2)) → 2NDSNEG(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2
2NDSNEG(mark(X1), X2) → 2NDSNEG(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2
2NDSNEG(X1, mark(X2)) → 2NDSNEG(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2
2NDSNEG(active(X1), X2) → 2NDSNEG(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

POSRECIP(mark(X)) → POSRECIP(X)
POSRECIP(active(X)) → POSRECIP(X)

The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

POSRECIP(mark(X)) → POSRECIP(X)
POSRECIP(active(X)) → POSRECIP(X)

From the DPs we obtained the following set of size-change graphs:

POSRECIP(mark(X)) → POSRECIP(X)
The graph contains the following edges 1 > 1
POSRECIP(active(X)) → POSRECIP(X)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

RCONS(X1, active(X2)) → RCONS(X1, X2)
RCONS(active(X1), X2) → RCONS(X1, X2)
RCONS(X1, mark(X2)) → RCONS(X1, X2)
RCONS(mark(X1), X2) → RCONS(X1, X2)

The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

RCONS(X1, active(X2)) → RCONS(X1, X2)
RCONS(active(X1), X2) → RCONS(X1, X2)
RCONS(X1, mark(X2)) → RCONS(X1, X2)
RCONS(mark(X1), X2) → RCONS(X1, X2)

From the DPs we obtained the following set of size-change graphs:

RCONS(X1, active(X2)) → RCONS(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2
RCONS(active(X1), X2) → RCONS(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2
RCONS(X1, mark(X2)) → RCONS(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2
RCONS(mark(X1), X2) → RCONS(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CONS2(mark(X1), X2) → CONS2(X1, X2)
CONS2(X1, active(X2)) → CONS2(X1, X2)
CONS2(X1, mark(X2)) → CONS2(X1, X2)
CONS2(active(X1), X2) → CONS2(X1, X2)

The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CONS2(mark(X1), X2) → CONS2(X1, X2)
CONS2(X1, mark(X2)) → CONS2(X1, X2)
CONS2(X1, active(X2)) → CONS2(X1, X2)
CONS2(active(X1), X2) → CONS2(X1, X2)

From the DPs we obtained the following set of size-change graphs:

CONS2(mark(X1), X2) → CONS2(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2
CONS2(X1, active(X2)) → CONS2(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2
CONS2(X1, mark(X2)) → CONS2(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2
CONS2(active(X1), X2) → CONS2(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

2NDSPOS(X1, active(X2)) → 2NDSPOS(X1, X2)
2NDSPOS(X1, mark(X2)) → 2NDSPOS(X1, X2)
2NDSPOS(active(X1), X2) → 2NDSPOS(X1, X2)
2NDSPOS(mark(X1), X2) → 2NDSPOS(X1, X2)

The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

2NDSPOS(X1, mark(X2)) → 2NDSPOS(X1, X2)
2NDSPOS(X1, active(X2)) → 2NDSPOS(X1, X2)
2NDSPOS(active(X1), X2) → 2NDSPOS(X1, X2)
2NDSPOS(mark(X1), X2) → 2NDSPOS(X1, X2)

From the DPs we obtained the following set of size-change graphs:

2NDSPOS(X1, active(X2)) → 2NDSPOS(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2
2NDSPOS(X1, mark(X2)) → 2NDSPOS(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2
2NDSPOS(active(X1), X2) → 2NDSPOS(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2
2NDSPOS(mark(X1), X2) → 2NDSPOS(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

S(mark(X)) → S(X)
S(active(X)) → S(X)

The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

S(active(X)) → S(X)
S(mark(X)) → S(X)

From the DPs we obtained the following set of size-change graphs:

S(mark(X)) → S(X)
The graph contains the following edges 1 > 1
S(active(X)) → S(X)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CONS(X1, active(X2)) → CONS(X1, X2)
CONS(mark(X1), X2) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)
CONS(X1, mark(X2)) → CONS(X1, X2)

The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

CONS(mark(X1), X2) → CONS(X1, X2)
CONS(X1, active(X2)) → CONS(X1, X2)
CONS(X1, mark(X2)) → CONS(X1, X2)
CONS(active(X1), X2) → CONS(X1, X2)

From the DPs we obtained the following set of size-change graphs:

CONS(X1, active(X2)) → CONS(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2
CONS(mark(X1), X2) → CONS(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2
CONS(active(X1), X2) → CONS(X1, X2)
The graph contains the following edges 1 > 1, 2 >= 2
CONS(X1, mark(X2)) → CONS(X1, X2)
The graph contains the following edges 1 >= 1, 2 > 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

FROM(mark(X)) → FROM(X)
FROM(active(X)) → FROM(X)

The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QDPSizeChangeProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

FROM(mark(X)) → FROM(X)
FROM(active(X)) → FROM(X)

From the DPs we obtained the following set of size-change graphs:

FROM(mark(X)) → FROM(X)
The graph contains the following edges 1 > 1
FROM(active(X)) → FROM(X)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(square(X)) → MARK(times(X, X))
ACTIVE(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → MARK(rcons(negrecip(Y), 2ndspos(N, Z)))
MARK(negrecip(X)) → ACTIVE(negrecip(mark(X)))
ACTIVE(times(s(X), Y)) → MARK(plus(Y, times(X, Y)))
MARK(2ndspos(X1, X2)) → MARK(X1)
MARK(s(X)) → MARK(X)
MARK(cons(X1, X2)) → MARK(X1)
MARK(times(X1, X2)) → MARK(X1)
MARK(pi(X)) → MARK(X)
MARK(2ndspos(X1, X2)) → MARK(X2)
ACTIVE(2ndsneg(s(N), cons(X, Z))) → MARK(2ndsneg(s(N), cons2(X, Z)))
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → MARK(X2)
ACTIVE(2ndspos(s(N), cons(X, Z))) → MARK(2ndspos(s(N), cons2(X, Z)))
MARK(posrecip(X)) → ACTIVE(posrecip(mark(X)))
MARK(plus(X1, X2)) → ACTIVE(plus(mark(X1), mark(X2)))
MARK(2ndspos(X1, X2)) → ACTIVE(2ndspos(mark(X1), mark(X2)))
MARK(negrecip(X)) → MARK(X)
MARK(2ndsneg(X1, X2)) → MARK(X1)
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(posrecip(X)) → MARK(X)
MARK(2ndsneg(X1, X2)) → MARK(X2)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
ACTIVE(pi(X)) → MARK(2ndspos(X, from(0)))
MARK(rcons(X1, X2)) → MARK(X1)
MARK(from(X)) → MARK(X)
ACTIVE(plus(0, Y)) → MARK(Y)
ACTIVE(2ndspos(s(N), cons2(X, cons(Y, Z)))) → MARK(rcons(posrecip(Y), 2ndsneg(N, Z)))
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(plus(X1, X2)) → MARK(X1)
MARK(square(X)) → MARK(X)
MARK(times(X1, X2)) → ACTIVE(times(mark(X1), mark(X2)))
MARK(cons2(X1, X2)) → ACTIVE(cons2(X1, mark(X2)))
MARK(2ndsneg(X1, X2)) → ACTIVE(2ndsneg(mark(X1), mark(X2)))
MARK(square(X)) → ACTIVE(square(mark(X)))
MARK(from(X)) → ACTIVE(from(mark(X)))
MARK(rcons(X1, X2)) → ACTIVE(rcons(mark(X1), mark(X2)))
MARK(rcons(X1, X2)) → MARK(X2)
MARK(pi(X)) → ACTIVE(pi(mark(X)))
ACTIVE(plus(s(X), Y)) → MARK(s(plus(X, Y)))
MARK(cons2(X1, X2)) → MARK(X2)

The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(negrecip(X)) → ACTIVE(negrecip(mark(X)))
MARK(posrecip(X)) → ACTIVE(posrecip(mark(X)))
MARK(s(X)) → ACTIVE(s(mark(X)))
MARK(cons(X1, X2)) → ACTIVE(cons(mark(X1), X2))
MARK(cons2(X1, X2)) → ACTIVE(cons2(X1, mark(X2)))
MARK(rcons(X1, X2)) → ACTIVE(rcons(mark(X1), mark(X2)))

The remaining pairs can at least be oriented weakly.

ACTIVE(square(X)) → MARK(times(X, X))
ACTIVE(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → MARK(rcons(negrecip(Y), 2ndspos(N, Z)))
ACTIVE(times(s(X), Y)) → MARK(plus(Y, times(X, Y)))
MARK(2ndspos(X1, X2)) → MARK(X1)
MARK(s(X)) → MARK(X)
MARK(cons(X1, X2)) → MARK(X1)
MARK(times(X1, X2)) → MARK(X1)
MARK(pi(X)) → MARK(X)
MARK(2ndspos(X1, X2)) → MARK(X2)
ACTIVE(2ndsneg(s(N), cons(X, Z))) → MARK(2ndsneg(s(N), cons2(X, Z)))
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → MARK(X2)
ACTIVE(2ndspos(s(N), cons(X, Z))) → MARK(2ndspos(s(N), cons2(X, Z)))
MARK(plus(X1, X2)) → ACTIVE(plus(mark(X1), mark(X2)))
MARK(2ndspos(X1, X2)) → ACTIVE(2ndspos(mark(X1), mark(X2)))
MARK(negrecip(X)) → MARK(X)
MARK(2ndsneg(X1, X2)) → MARK(X1)
MARK(posrecip(X)) → MARK(X)
MARK(2ndsneg(X1, X2)) → MARK(X2)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
ACTIVE(pi(X)) → MARK(2ndspos(X, from(0)))
MARK(rcons(X1, X2)) → MARK(X1)
MARK(from(X)) → MARK(X)
ACTIVE(plus(0, Y)) → MARK(Y)
ACTIVE(2ndspos(s(N), cons2(X, cons(Y, Z)))) → MARK(rcons(posrecip(Y), 2ndsneg(N, Z)))
MARK(plus(X1, X2)) → MARK(X1)
MARK(square(X)) → MARK(X)
MARK(times(X1, X2)) → ACTIVE(times(mark(X1), mark(X2)))
MARK(2ndsneg(X1, X2)) → ACTIVE(2ndsneg(mark(X1), mark(X2)))
MARK(square(X)) → ACTIVE(square(mark(X)))
MARK(from(X)) → ACTIVE(from(mark(X)))
MARK(rcons(X1, X2)) → MARK(X2)
MARK(pi(X)) → ACTIVE(pi(mark(X)))
ACTIVE(plus(s(X), Y)) → MARK(s(plus(X, Y)))
MARK(cons2(X1, X2)) → MARK(X2)

Used ordering: Polynomial interpretation with max and min functions [25]:

POL(0) = 0
POL(2ndsneg(x₁, x₂)) = 1
POL(2ndspos(x₁, x₂)) = 1
POL(ACTIVE(x₁)) = x₁
POL(MARK(x₁)) = 1
POL(active(x₁)) = 0
POL(cons(x₁, x₂)) = 0
POL(cons2(x₁, x₂)) = 0
POL(from(x₁)) = 1
POL(mark(x₁)) = 0
POL(negrecip(x₁)) = 0
POL(pi(x₁)) = 1
POL(plus(x₁, x₂)) = 1
POL(posrecip(x₁)) = 0
POL(rcons(x₁, x₂)) = 0
POL(rnil) = 0
POL(s(x₁)) = 0
POL(square(x₁)) = 1
POL(times(x₁, x₂)) = 1

The following usable rules [17] were oriented:

plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
plus(mark(X1), X2) → plus(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
posrecip(active(X)) → posrecip(X)
posrecip(mark(X)) → posrecip(X)
square(active(X)) → square(X)
square(mark(X)) → square(X)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
times(mark(X1), X2) → times(X1, X2)
from(active(X)) → from(X)
from(mark(X)) → from(X)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
s(active(X)) → s(X)
s(mark(X)) → s(X)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(square(X)) → MARK(times(X, X))
ACTIVE(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → MARK(rcons(negrecip(Y), 2ndspos(N, Z)))
MARK(s(X)) → MARK(X)
MARK(2ndspos(X1, X2)) → MARK(X1)
ACTIVE(times(s(X), Y)) → MARK(plus(Y, times(X, Y)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(2ndspos(X1, X2)) → MARK(X2)
MARK(pi(X)) → MARK(X)
MARK(times(X1, X2)) → MARK(X1)
ACTIVE(2ndsneg(s(N), cons(X, Z))) → MARK(2ndsneg(s(N), cons2(X, Z)))
MARK(plus(X1, X2)) → MARK(X2)
MARK(times(X1, X2)) → MARK(X2)
ACTIVE(2ndspos(s(N), cons(X, Z))) → MARK(2ndspos(s(N), cons2(X, Z)))
MARK(plus(X1, X2)) → ACTIVE(plus(mark(X1), mark(X2)))
MARK(2ndspos(X1, X2)) → ACTIVE(2ndspos(mark(X1), mark(X2)))
MARK(negrecip(X)) → MARK(X)
MARK(2ndsneg(X1, X2)) → MARK(X1)
MARK(posrecip(X)) → MARK(X)
MARK(2ndsneg(X1, X2)) → MARK(X2)
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
ACTIVE(pi(X)) → MARK(2ndspos(X, from(0)))
MARK(rcons(X1, X2)) → MARK(X1)
MARK(from(X)) → MARK(X)
ACTIVE(plus(0, Y)) → MARK(Y)
ACTIVE(2ndspos(s(N), cons2(X, cons(Y, Z)))) → MARK(rcons(posrecip(Y), 2ndsneg(N, Z)))
MARK(plus(X1, X2)) → MARK(X1)
MARK(times(X1, X2)) → ACTIVE(times(mark(X1), mark(X2)))
MARK(square(X)) → MARK(X)
MARK(2ndsneg(X1, X2)) → ACTIVE(2ndsneg(mark(X1), mark(X2)))
MARK(square(X)) → ACTIVE(square(mark(X)))
MARK(from(X)) → ACTIVE(from(mark(X)))
MARK(rcons(X1, X2)) → MARK(X2)
ACTIVE(plus(s(X), Y)) → MARK(s(plus(X, Y)))
MARK(pi(X)) → ACTIVE(pi(mark(X)))
MARK(cons2(X1, X2)) → MARK(X2)

The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(plus(X1, X2)) → ACTIVE(plus(mark(X1), mark(X2))) at position [0] we obtained the following new rules:

MARK(plus(y0, from(x0))) → ACTIVE(plus(mark(y0), active(from(mark(x0)))))
MARK(plus(cons2(x0, x1), y1)) → ACTIVE(plus(active(cons2(x0, mark(x1))), mark(y1)))
MARK(plus(y0, plus(x0, x1))) → ACTIVE(plus(mark(y0), active(plus(mark(x0), mark(x1)))))
MARK(plus(y0, 2ndsneg(x0, x1))) → ACTIVE(plus(mark(y0), active(2ndsneg(mark(x0), mark(x1)))))
MARK(plus(rcons(x0, x1), y1)) → ACTIVE(plus(active(rcons(mark(x0), mark(x1))), mark(y1)))
MARK(plus(y0, square(x0))) → ACTIVE(plus(mark(y0), active(square(mark(x0)))))
MARK(plus(y0, 2ndspos(x0, x1))) → ACTIVE(plus(mark(y0), active(2ndspos(mark(x0), mark(x1)))))
MARK(plus(y0, negrecip(x0))) → ACTIVE(plus(mark(y0), active(negrecip(mark(x0)))))
MARK(plus(y0, cons2(x0, x1))) → ACTIVE(plus(mark(y0), active(cons2(x0, mark(x1)))))
MARK(plus(2ndspos(x0, x1), y1)) → ACTIVE(plus(active(2ndspos(mark(x0), mark(x1))), mark(y1)))
MARK(plus(square(x0), y1)) → ACTIVE(plus(active(square(mark(x0))), mark(y1)))
MARK(plus(y0, cons(x0, x1))) → ACTIVE(plus(mark(y0), active(cons(mark(x0), x1))))
MARK(plus(y0, rcons(x0, x1))) → ACTIVE(plus(mark(y0), active(rcons(mark(x0), mark(x1)))))
MARK(plus(x0, y1)) → ACTIVE(plus(x0, mark(y1)))
MARK(plus(y0, pi(x0))) → ACTIVE(plus(mark(y0), active(pi(mark(x0)))))
MARK(plus(y0, x1)) → ACTIVE(plus(mark(y0), x1))
MARK(plus(pi(x0), y1)) → ACTIVE(plus(active(pi(mark(x0))), mark(y1)))
MARK(plus(negrecip(x0), y1)) → ACTIVE(plus(active(negrecip(mark(x0))), mark(y1)))
MARK(plus(y0, s(x0))) → ACTIVE(plus(mark(y0), active(s(mark(x0)))))
MARK(plus(y0, posrecip(x0))) → ACTIVE(plus(mark(y0), active(posrecip(mark(x0)))))
MARK(plus(s(x0), y1)) → ACTIVE(plus(active(s(mark(x0))), mark(y1)))
MARK(plus(2ndsneg(x0, x1), y1)) → ACTIVE(plus(active(2ndsneg(mark(x0), mark(x1))), mark(y1)))
MARK(plus(times(x0, x1), y1)) → ACTIVE(plus(active(times(mark(x0), mark(x1))), mark(y1)))
MARK(plus(0, y1)) → ACTIVE(plus(active(0), mark(y1)))
MARK(plus(y0, 0)) → ACTIVE(plus(mark(y0), active(0)))
MARK(plus(plus(x0, x1), y1)) → ACTIVE(plus(active(plus(mark(x0), mark(x1))), mark(y1)))
MARK(plus(posrecip(x0), y1)) → ACTIVE(plus(active(posrecip(mark(x0))), mark(y1)))
MARK(plus(from(x0), y1)) → ACTIVE(plus(active(from(mark(x0))), mark(y1)))
MARK(plus(rnil, y1)) → ACTIVE(plus(active(rnil), mark(y1)))
MARK(plus(cons(x0, x1), y1)) → ACTIVE(plus(active(cons(mark(x0), x1)), mark(y1)))
MARK(plus(y0, rnil)) → ACTIVE(plus(mark(y0), active(rnil)))
MARK(plus(y0, times(x0, x1))) → ACTIVE(plus(mark(y0), active(times(mark(x0), mark(x1)))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → MARK(rcons(negrecip(Y), 2ndspos(N, Z)))
ACTIVE(times(s(X), Y)) → MARK(plus(Y, times(X, Y)))
MARK(plus(cons2(x0, x1), y1)) → ACTIVE(plus(active(cons2(x0, mark(x1))), mark(y1)))
MARK(plus(y0, square(x0))) → ACTIVE(plus(mark(y0), active(square(mark(x0)))))
MARK(cons(X1, X2)) → MARK(X1)
MARK(2ndspos(X1, X2)) → MARK(X2)
ACTIVE(2ndsneg(s(N), cons(X, Z))) → MARK(2ndsneg(s(N), cons2(X, Z)))
MARK(plus(y0, negrecip(x0))) → ACTIVE(plus(mark(y0), active(negrecip(mark(x0)))))
MARK(times(X1, X2)) → MARK(X2)
ACTIVE(2ndspos(s(N), cons(X, Z))) → MARK(2ndspos(s(N), cons2(X, Z)))
MARK(plus(square(x0), y1)) → ACTIVE(plus(active(square(mark(x0))), mark(y1)))
MARK(2ndspos(X1, X2)) → ACTIVE(2ndspos(mark(X1), mark(X2)))
MARK(plus(y0, cons(x0, x1))) → ACTIVE(plus(mark(y0), active(cons(mark(x0), x1))))
MARK(plus(y0, rcons(x0, x1))) → ACTIVE(plus(mark(y0), active(rcons(mark(x0), mark(x1)))))
MARK(2ndsneg(X1, X2)) → MARK(X1)
MARK(plus(x0, y1)) → ACTIVE(plus(x0, mark(y1)))
MARK(plus(y0, x1)) → ACTIVE(plus(mark(y0), x1))
MARK(plus(y0, pi(x0))) → ACTIVE(plus(mark(y0), active(pi(mark(x0)))))
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(rcons(X1, X2)) → MARK(X1)
MARK(plus(negrecip(x0), y1)) → ACTIVE(plus(active(negrecip(mark(x0))), mark(y1)))
MARK(plus(y0, s(x0))) → ACTIVE(plus(mark(y0), active(s(mark(x0)))))
ACTIVE(plus(0, Y)) → MARK(Y)
MARK(plus(times(x0, x1), y1)) → ACTIVE(plus(active(times(mark(x0), mark(x1))), mark(y1)))
MARK(square(X)) → MARK(X)
MARK(2ndsneg(X1, X2)) → ACTIVE(2ndsneg(mark(X1), mark(X2)))
MARK(rcons(X1, X2)) → MARK(X2)
MARK(cons2(X1, X2)) → MARK(X2)
ACTIVE(square(X)) → MARK(times(X, X))
MARK(plus(y0, from(x0))) → ACTIVE(plus(mark(y0), active(from(mark(x0)))))
MARK(s(X)) → MARK(X)
MARK(2ndspos(X1, X2)) → MARK(X1)
MARK(plus(y0, plus(x0, x1))) → ACTIVE(plus(mark(y0), active(plus(mark(x0), mark(x1)))))
MARK(plus(y0, 2ndsneg(x0, x1))) → ACTIVE(plus(mark(y0), active(2ndsneg(mark(x0), mark(x1)))))
MARK(plus(rcons(x0, x1), y1)) → ACTIVE(plus(active(rcons(mark(x0), mark(x1))), mark(y1)))
MARK(pi(X)) → MARK(X)
MARK(times(X1, X2)) → MARK(X1)
MARK(plus(y0, 2ndspos(x0, x1))) → ACTIVE(plus(mark(y0), active(2ndspos(mark(x0), mark(x1)))))
MARK(plus(X1, X2)) → MARK(X2)
MARK(plus(y0, cons2(x0, x1))) → ACTIVE(plus(mark(y0), active(cons2(x0, mark(x1)))))
MARK(plus(2ndspos(x0, x1), y1)) → ACTIVE(plus(active(2ndspos(mark(x0), mark(x1))), mark(y1)))
MARK(negrecip(X)) → MARK(X)
MARK(posrecip(X)) → MARK(X)
MARK(2ndsneg(X1, X2)) → MARK(X2)
ACTIVE(pi(X)) → MARK(2ndspos(X, from(0)))
MARK(plus(pi(x0), y1)) → ACTIVE(plus(active(pi(mark(x0))), mark(y1)))
MARK(from(X)) → MARK(X)
ACTIVE(2ndspos(s(N), cons2(X, cons(Y, Z)))) → MARK(rcons(posrecip(Y), 2ndsneg(N, Z)))
MARK(plus(s(x0), y1)) → ACTIVE(plus(active(s(mark(x0))), mark(y1)))
MARK(plus(y0, posrecip(x0))) → ACTIVE(plus(mark(y0), active(posrecip(mark(x0)))))
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(2ndsneg(x0, x1), y1)) → ACTIVE(plus(active(2ndsneg(mark(x0), mark(x1))), mark(y1)))
MARK(times(X1, X2)) → ACTIVE(times(mark(X1), mark(X2)))
MARK(plus(y0, 0)) → ACTIVE(plus(mark(y0), active(0)))
MARK(plus(0, y1)) → ACTIVE(plus(active(0), mark(y1)))
MARK(plus(plus(x0, x1), y1)) → ACTIVE(plus(active(plus(mark(x0), mark(x1))), mark(y1)))
MARK(square(X)) → ACTIVE(square(mark(X)))
MARK(plus(posrecip(x0), y1)) → ACTIVE(plus(active(posrecip(mark(x0))), mark(y1)))
MARK(plus(from(x0), y1)) → ACTIVE(plus(active(from(mark(x0))), mark(y1)))
MARK(plus(y0, rnil)) → ACTIVE(plus(mark(y0), active(rnil)))
MARK(plus(cons(x0, x1), y1)) → ACTIVE(plus(active(cons(mark(x0), x1)), mark(y1)))
MARK(plus(rnil, y1)) → ACTIVE(plus(active(rnil), mark(y1)))
MARK(plus(y0, times(x0, x1))) → ACTIVE(plus(mark(y0), active(times(mark(x0), mark(x1)))))
MARK(from(X)) → ACTIVE(from(mark(X)))
ACTIVE(plus(s(X), Y)) → MARK(s(plus(X, Y)))
MARK(pi(X)) → ACTIVE(pi(mark(X)))

The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(2ndspos(X1, X2)) → ACTIVE(2ndspos(mark(X1), mark(X2))) at position [0] we obtained the following new rules:

MARK(2ndspos(y0, pi(x0))) → ACTIVE(2ndspos(mark(y0), active(pi(mark(x0)))))
MARK(2ndspos(2ndspos(x0, x1), y1)) → ACTIVE(2ndspos(active(2ndspos(mark(x0), mark(x1))), mark(y1)))
MARK(2ndspos(0, y1)) → ACTIVE(2ndspos(active(0), mark(y1)))
MARK(2ndspos(y0, 0)) → ACTIVE(2ndspos(mark(y0), active(0)))
MARK(2ndspos(y0, from(x0))) → ACTIVE(2ndspos(mark(y0), active(from(mark(x0)))))
MARK(2ndspos(y0, square(x0))) → ACTIVE(2ndspos(mark(y0), active(square(mark(x0)))))
MARK(2ndspos(2ndsneg(x0, x1), y1)) → ACTIVE(2ndspos(active(2ndsneg(mark(x0), mark(x1))), mark(y1)))
MARK(2ndspos(cons(x0, x1), y1)) → ACTIVE(2ndspos(active(cons(mark(x0), x1)), mark(y1)))
MARK(2ndspos(negrecip(x0), y1)) → ACTIVE(2ndspos(active(negrecip(mark(x0))), mark(y1)))
MARK(2ndspos(square(x0), y1)) → ACTIVE(2ndspos(active(square(mark(x0))), mark(y1)))
MARK(2ndspos(y0, negrecip(x0))) → ACTIVE(2ndspos(mark(y0), active(negrecip(mark(x0)))))
MARK(2ndspos(from(x0), y1)) → ACTIVE(2ndspos(active(from(mark(x0))), mark(y1)))
MARK(2ndspos(y0, posrecip(x0))) → ACTIVE(2ndspos(mark(y0), active(posrecip(mark(x0)))))
MARK(2ndspos(y0, 2ndspos(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(2ndspos(mark(x0), mark(x1)))))
MARK(2ndspos(y0, 2ndsneg(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(2ndsneg(mark(x0), mark(x1)))))
MARK(2ndspos(cons2(x0, x1), y1)) → ACTIVE(2ndspos(active(cons2(x0, mark(x1))), mark(y1)))
MARK(2ndspos(y0, cons2(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(cons2(x0, mark(x1)))))
MARK(2ndspos(posrecip(x0), y1)) → ACTIVE(2ndspos(active(posrecip(mark(x0))), mark(y1)))
MARK(2ndspos(pi(x0), y1)) → ACTIVE(2ndspos(active(pi(mark(x0))), mark(y1)))
MARK(2ndspos(y0, rcons(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(rcons(mark(x0), mark(x1)))))
MARK(2ndspos(y0, cons(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(cons(mark(x0), x1))))
MARK(2ndspos(x0, y1)) → ACTIVE(2ndspos(x0, mark(y1)))
MARK(2ndspos(rcons(x0, x1), y1)) → ACTIVE(2ndspos(active(rcons(mark(x0), mark(x1))), mark(y1)))
MARK(2ndspos(times(x0, x1), y1)) → ACTIVE(2ndspos(active(times(mark(x0), mark(x1))), mark(y1)))
MARK(2ndspos(y0, plus(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(plus(mark(x0), mark(x1)))))
MARK(2ndspos(y0, x1)) → ACTIVE(2ndspos(mark(y0), x1))
MARK(2ndspos(y0, s(x0))) → ACTIVE(2ndspos(mark(y0), active(s(mark(x0)))))
MARK(2ndspos(plus(x0, x1), y1)) → ACTIVE(2ndspos(active(plus(mark(x0), mark(x1))), mark(y1)))
MARK(2ndspos(y0, times(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(times(mark(x0), mark(x1)))))
MARK(2ndspos(rnil, y1)) → ACTIVE(2ndspos(active(rnil), mark(y1)))
MARK(2ndspos(y0, rnil)) → ACTIVE(2ndspos(mark(y0), active(rnil)))
MARK(2ndspos(s(x0), y1)) → ACTIVE(2ndspos(active(s(mark(x0))), mark(y1)))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(times(s(X), Y)) → MARK(plus(Y, times(X, Y)))
MARK(2ndspos(y0, from(x0))) → ACTIVE(2ndspos(mark(y0), active(from(mark(x0)))))
MARK(2ndspos(X1, X2)) → MARK(X2)
MARK(2ndspos(negrecip(x0), y1)) → ACTIVE(2ndspos(active(negrecip(mark(x0))), mark(y1)))
MARK(plus(y0, negrecip(x0))) → ACTIVE(plus(mark(y0), active(negrecip(mark(x0)))))
MARK(plus(square(x0), y1)) → ACTIVE(plus(active(square(mark(x0))), mark(y1)))
MARK(plus(y0, rcons(x0, x1))) → ACTIVE(plus(mark(y0), active(rcons(mark(x0), mark(x1)))))
MARK(plus(x0, y1)) → ACTIVE(plus(x0, mark(y1)))
MARK(2ndspos(y0, cons2(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(cons2(x0, mark(x1)))))
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(2ndspos(posrecip(x0), y1)) → ACTIVE(2ndspos(active(posrecip(mark(x0))), mark(y1)))
MARK(2ndspos(pi(x0), y1)) → ACTIVE(2ndspos(active(pi(mark(x0))), mark(y1)))
MARK(2ndspos(y0, rcons(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(rcons(mark(x0), mark(x1)))))
MARK(plus(negrecip(x0), y1)) → ACTIVE(plus(active(negrecip(mark(x0))), mark(y1)))
ACTIVE(plus(0, Y)) → MARK(Y)
MARK(2ndsneg(X1, X2)) → ACTIVE(2ndsneg(mark(X1), mark(X2)))
MARK(cons2(X1, X2)) → MARK(X2)
MARK(2ndspos(y0, pi(x0))) → ACTIVE(2ndspos(mark(y0), active(pi(mark(x0)))))
ACTIVE(square(X)) → MARK(times(X, X))
MARK(plus(y0, from(x0))) → ACTIVE(plus(mark(y0), active(from(mark(x0)))))
MARK(s(X)) → MARK(X)
MARK(2ndspos(X1, X2)) → MARK(X1)
MARK(plus(rcons(x0, x1), y1)) → ACTIVE(plus(active(rcons(mark(x0), mark(x1))), mark(y1)))
MARK(pi(X)) → MARK(X)
MARK(2ndspos(square(x0), y1)) → ACTIVE(2ndspos(active(square(mark(x0))), mark(y1)))
MARK(plus(X1, X2)) → MARK(X2)
MARK(2ndspos(y0, posrecip(x0))) → ACTIVE(2ndspos(mark(y0), active(posrecip(mark(x0)))))
MARK(2ndspos(y0, 2ndspos(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(2ndspos(mark(x0), mark(x1)))))
MARK(2ndspos(y0, 2ndsneg(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(2ndsneg(mark(x0), mark(x1)))))
MARK(2ndspos(cons2(x0, x1), y1)) → ACTIVE(2ndspos(active(cons2(x0, mark(x1))), mark(y1)))
MARK(2ndsneg(X1, X2)) → MARK(X2)
ACTIVE(2ndspos(s(N), cons2(X, cons(Y, Z)))) → MARK(rcons(posrecip(Y), 2ndsneg(N, Z)))
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(2ndsneg(x0, x1), y1)) → ACTIVE(plus(active(2ndsneg(mark(x0), mark(x1))), mark(y1)))
MARK(times(X1, X2)) → ACTIVE(times(mark(X1), mark(X2)))
MARK(plus(y0, 0)) → ACTIVE(plus(mark(y0), active(0)))
MARK(plus(0, y1)) → ACTIVE(plus(active(0), mark(y1)))
MARK(plus(plus(x0, x1), y1)) → ACTIVE(plus(active(plus(mark(x0), mark(x1))), mark(y1)))
MARK(square(X)) → ACTIVE(square(mark(X)))
MARK(2ndspos(rcons(x0, x1), y1)) → ACTIVE(2ndspos(active(rcons(mark(x0), mark(x1))), mark(y1)))
MARK(2ndspos(y0, plus(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(plus(mark(x0), mark(x1)))))
MARK(2ndspos(y0, x1)) → ACTIVE(2ndspos(mark(y0), x1))
MARK(plus(from(x0), y1)) → ACTIVE(plus(active(from(mark(x0))), mark(y1)))
MARK(plus(y0, rnil)) → ACTIVE(plus(mark(y0), active(rnil)))
MARK(plus(cons(x0, x1), y1)) → ACTIVE(plus(active(cons(mark(x0), x1)), mark(y1)))
MARK(plus(rnil, y1)) → ACTIVE(plus(active(rnil), mark(y1)))
MARK(plus(y0, times(x0, x1))) → ACTIVE(plus(mark(y0), active(times(mark(x0), mark(x1)))))
MARK(2ndspos(plus(x0, x1), y1)) → ACTIVE(2ndspos(active(plus(mark(x0), mark(x1))), mark(y1)))
MARK(2ndspos(s(x0), y1)) → ACTIVE(2ndspos(active(s(mark(x0))), mark(y1)))
ACTIVE(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → MARK(rcons(negrecip(Y), 2ndspos(N, Z)))
MARK(2ndspos(2ndspos(x0, x1), y1)) → ACTIVE(2ndspos(active(2ndspos(mark(x0), mark(x1))), mark(y1)))
MARK(2ndspos(0, y1)) → ACTIVE(2ndspos(active(0), mark(y1)))
MARK(2ndspos(y0, 0)) → ACTIVE(2ndspos(mark(y0), active(0)))
MARK(plus(cons2(x0, x1), y1)) → ACTIVE(plus(active(cons2(x0, mark(x1))), mark(y1)))
MARK(2ndspos(y0, square(x0))) → ACTIVE(2ndspos(mark(y0), active(square(mark(x0)))))
MARK(plus(y0, square(x0))) → ACTIVE(plus(mark(y0), active(square(mark(x0)))))
MARK(2ndspos(2ndsneg(x0, x1), y1)) → ACTIVE(2ndspos(active(2ndsneg(mark(x0), mark(x1))), mark(y1)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(2ndspos(cons(x0, x1), y1)) → ACTIVE(2ndspos(active(cons(mark(x0), x1)), mark(y1)))
ACTIVE(2ndsneg(s(N), cons(X, Z))) → MARK(2ndsneg(s(N), cons2(X, Z)))
MARK(2ndspos(y0, negrecip(x0))) → ACTIVE(2ndspos(mark(y0), active(negrecip(mark(x0)))))
MARK(times(X1, X2)) → MARK(X2)
ACTIVE(2ndspos(s(N), cons(X, Z))) → MARK(2ndspos(s(N), cons2(X, Z)))
MARK(plus(y0, cons(x0, x1))) → ACTIVE(plus(mark(y0), active(cons(mark(x0), x1))))
MARK(2ndsneg(X1, X2)) → MARK(X1)
MARK(plus(y0, x1)) → ACTIVE(plus(mark(y0), x1))
MARK(plus(y0, pi(x0))) → ACTIVE(plus(mark(y0), active(pi(mark(x0)))))
MARK(rcons(X1, X2)) → MARK(X1)
MARK(plus(y0, s(x0))) → ACTIVE(plus(mark(y0), active(s(mark(x0)))))
MARK(plus(times(x0, x1), y1)) → ACTIVE(plus(active(times(mark(x0), mark(x1))), mark(y1)))
MARK(square(X)) → MARK(X)
MARK(2ndspos(times(x0, x1), y1)) → ACTIVE(2ndspos(active(times(mark(x0), mark(x1))), mark(y1)))
MARK(rcons(X1, X2)) → MARK(X2)
MARK(2ndspos(rnil, y1)) → ACTIVE(2ndspos(active(rnil), mark(y1)))
MARK(2ndspos(y0, rnil)) → ACTIVE(2ndspos(mark(y0), active(rnil)))
MARK(plus(y0, plus(x0, x1))) → ACTIVE(plus(mark(y0), active(plus(mark(x0), mark(x1)))))
MARK(plus(y0, 2ndsneg(x0, x1))) → ACTIVE(plus(mark(y0), active(2ndsneg(mark(x0), mark(x1)))))
MARK(times(X1, X2)) → MARK(X1)
MARK(plus(y0, 2ndspos(x0, x1))) → ACTIVE(plus(mark(y0), active(2ndspos(mark(x0), mark(x1)))))
MARK(plus(y0, cons2(x0, x1))) → ACTIVE(plus(mark(y0), active(cons2(x0, mark(x1)))))
MARK(plus(2ndspos(x0, x1), y1)) → ACTIVE(plus(active(2ndspos(mark(x0), mark(x1))), mark(y1)))
MARK(2ndspos(from(x0), y1)) → ACTIVE(2ndspos(active(from(mark(x0))), mark(y1)))
MARK(negrecip(X)) → MARK(X)
MARK(posrecip(X)) → MARK(X)
ACTIVE(pi(X)) → MARK(2ndspos(X, from(0)))
MARK(plus(pi(x0), y1)) → ACTIVE(plus(active(pi(mark(x0))), mark(y1)))
MARK(from(X)) → MARK(X)
MARK(2ndspos(y0, cons(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(cons(mark(x0), x1))))
MARK(plus(s(x0), y1)) → ACTIVE(plus(active(s(mark(x0))), mark(y1)))
MARK(plus(y0, posrecip(x0))) → ACTIVE(plus(mark(y0), active(posrecip(mark(x0)))))
MARK(2ndspos(x0, y1)) → ACTIVE(2ndspos(x0, mark(y1)))
MARK(plus(posrecip(x0), y1)) → ACTIVE(plus(active(posrecip(mark(x0))), mark(y1)))
MARK(2ndspos(y0, s(x0))) → ACTIVE(2ndspos(mark(y0), active(s(mark(x0)))))
MARK(from(X)) → ACTIVE(from(mark(X)))
MARK(2ndspos(y0, times(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(times(mark(x0), mark(x1)))))
ACTIVE(plus(s(X), Y)) → MARK(s(plus(X, Y)))
MARK(pi(X)) → ACTIVE(pi(mark(X)))

The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(times(X1, X2)) → ACTIVE(times(mark(X1), mark(X2))) at position [0] we obtained the following new rules:

MARK(times(y0, pi(x0))) → ACTIVE(times(mark(y0), active(pi(mark(x0)))))
MARK(times(y0, x1)) → ACTIVE(times(mark(y0), x1))
MARK(times(square(x0), y1)) → ACTIVE(times(active(square(mark(x0))), mark(y1)))
MARK(times(cons(x0, x1), y1)) → ACTIVE(times(active(cons(mark(x0), x1)), mark(y1)))
MARK(times(pi(x0), y1)) → ACTIVE(times(active(pi(mark(x0))), mark(y1)))
MARK(times(plus(x0, x1), y1)) → ACTIVE(times(active(plus(mark(x0), mark(x1))), mark(y1)))
MARK(times(y0, plus(x0, x1))) → ACTIVE(times(mark(y0), active(plus(mark(x0), mark(x1)))))
MARK(times(y0, rcons(x0, x1))) → ACTIVE(times(mark(y0), active(rcons(mark(x0), mark(x1)))))
MARK(times(cons2(x0, x1), y1)) → ACTIVE(times(active(cons2(x0, mark(x1))), mark(y1)))
MARK(times(0, y1)) → ACTIVE(times(active(0), mark(y1)))
MARK(times(y0, 0)) → ACTIVE(times(mark(y0), active(0)))
MARK(times(2ndspos(x0, x1), y1)) → ACTIVE(times(active(2ndspos(mark(x0), mark(x1))), mark(y1)))
MARK(times(times(x0, x1), y1)) → ACTIVE(times(active(times(mark(x0), mark(x1))), mark(y1)))
MARK(times(y0, 2ndsneg(x0, x1))) → ACTIVE(times(mark(y0), active(2ndsneg(mark(x0), mark(x1)))))
MARK(times(posrecip(x0), y1)) → ACTIVE(times(active(posrecip(mark(x0))), mark(y1)))
MARK(times(y0, negrecip(x0))) → ACTIVE(times(mark(y0), active(negrecip(mark(x0)))))
MARK(times(s(x0), y1)) → ACTIVE(times(active(s(mark(x0))), mark(y1)))
MARK(times(y0, cons(x0, x1))) → ACTIVE(times(mark(y0), active(cons(mark(x0), x1))))
MARK(times(y0, cons2(x0, x1))) → ACTIVE(times(mark(y0), active(cons2(x0, mark(x1)))))
MARK(times(y0, square(x0))) → ACTIVE(times(mark(y0), active(square(mark(x0)))))
MARK(times(rcons(x0, x1), y1)) → ACTIVE(times(active(rcons(mark(x0), mark(x1))), mark(y1)))
MARK(times(y0, 2ndspos(x0, x1))) → ACTIVE(times(mark(y0), active(2ndspos(mark(x0), mark(x1)))))
MARK(times(y0, posrecip(x0))) → ACTIVE(times(mark(y0), active(posrecip(mark(x0)))))
MARK(times(x0, y1)) → ACTIVE(times(x0, mark(y1)))
MARK(times(y0, from(x0))) → ACTIVE(times(mark(y0), active(from(mark(x0)))))
MARK(times(rnil, y1)) → ACTIVE(times(active(rnil), mark(y1)))
MARK(times(y0, rnil)) → ACTIVE(times(mark(y0), active(rnil)))
MARK(times(y0, s(x0))) → ACTIVE(times(mark(y0), active(s(mark(x0)))))
MARK(times(2ndsneg(x0, x1), y1)) → ACTIVE(times(active(2ndsneg(mark(x0), mark(x1))), mark(y1)))
MARK(times(y0, times(x0, x1))) → ACTIVE(times(mark(y0), active(times(mark(x0), mark(x1)))))
MARK(times(from(x0), y1)) → ACTIVE(times(active(from(mark(x0))), mark(y1)))
MARK(times(negrecip(x0), y1)) → ACTIVE(times(active(negrecip(mark(x0))), mark(y1)))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

MARK(2ndspos(y0, from(x0))) → ACTIVE(2ndspos(mark(y0), active(from(mark(x0)))))
ACTIVE(times(s(X), Y)) → MARK(plus(Y, times(X, Y)))
MARK(2ndspos(negrecip(x0), y1)) → ACTIVE(2ndspos(active(negrecip(mark(x0))), mark(y1)))
MARK(2ndspos(X1, X2)) → MARK(X2)
MARK(plus(y0, negrecip(x0))) → ACTIVE(plus(mark(y0), active(negrecip(mark(x0)))))
MARK(plus(square(x0), y1)) → ACTIVE(plus(active(square(mark(x0))), mark(y1)))
MARK(times(cons(x0, x1), y1)) → ACTIVE(times(active(cons(mark(x0), x1)), mark(y1)))
MARK(plus(y0, rcons(x0, x1))) → ACTIVE(plus(mark(y0), active(rcons(mark(x0), mark(x1)))))
MARK(2ndspos(y0, cons2(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(cons2(x0, mark(x1)))))
MARK(plus(x0, y1)) → ACTIVE(plus(x0, mark(y1)))
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(2ndspos(y0, rcons(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(rcons(mark(x0), mark(x1)))))
MARK(2ndspos(pi(x0), y1)) → ACTIVE(2ndspos(active(pi(mark(x0))), mark(y1)))
MARK(2ndspos(posrecip(x0), y1)) → ACTIVE(2ndspos(active(posrecip(mark(x0))), mark(y1)))
MARK(times(y0, 0)) → ACTIVE(times(mark(y0), active(0)))
MARK(times(0, y1)) → ACTIVE(times(active(0), mark(y1)))
MARK(plus(negrecip(x0), y1)) → ACTIVE(plus(active(negrecip(mark(x0))), mark(y1)))
ACTIVE(plus(0, Y)) → MARK(Y)
MARK(2ndsneg(X1, X2)) → ACTIVE(2ndsneg(mark(X1), mark(X2)))
MARK(times(y0, posrecip(x0))) → ACTIVE(times(mark(y0), active(posrecip(mark(x0)))))
MARK(times(y0, from(x0))) → ACTIVE(times(mark(y0), active(from(mark(x0)))))
MARK(times(y0, rnil)) → ACTIVE(times(mark(y0), active(rnil)))
MARK(times(rnil, y1)) → ACTIVE(times(active(rnil), mark(y1)))
MARK(times(y0, times(x0, x1))) → ACTIVE(times(mark(y0), active(times(mark(x0), mark(x1)))))
MARK(cons2(X1, X2)) → MARK(X2)
MARK(2ndspos(y0, pi(x0))) → ACTIVE(2ndspos(mark(y0), active(pi(mark(x0)))))
ACTIVE(square(X)) → MARK(times(X, X))
MARK(plus(y0, from(x0))) → ACTIVE(plus(mark(y0), active(from(mark(x0)))))
MARK(2ndspos(X1, X2)) → MARK(X1)
MARK(s(X)) → MARK(X)
MARK(plus(rcons(x0, x1), y1)) → ACTIVE(plus(active(rcons(mark(x0), mark(x1))), mark(y1)))
MARK(pi(X)) → MARK(X)
MARK(2ndspos(square(x0), y1)) → ACTIVE(2ndspos(active(square(mark(x0))), mark(y1)))
MARK(plus(X1, X2)) → MARK(X2)
MARK(2ndspos(y0, 2ndspos(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(2ndspos(mark(x0), mark(x1)))))
MARK(2ndspos(y0, posrecip(x0))) → ACTIVE(2ndspos(mark(y0), active(posrecip(mark(x0)))))
MARK(2ndspos(y0, 2ndsneg(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(2ndsneg(mark(x0), mark(x1)))))
MARK(2ndspos(cons2(x0, x1), y1)) → ACTIVE(2ndspos(active(cons2(x0, mark(x1))), mark(y1)))
MARK(2ndsneg(X1, X2)) → MARK(X2)
ACTIVE(2ndspos(s(N), cons2(X, cons(Y, Z)))) → MARK(rcons(posrecip(Y), 2ndsneg(N, Z)))
MARK(times(times(x0, x1), y1)) → ACTIVE(times(active(times(mark(x0), mark(x1))), mark(y1)))
MARK(plus(X1, X2)) → MARK(X1)
MARK(times(y0, 2ndsneg(x0, x1))) → ACTIVE(times(mark(y0), active(2ndsneg(mark(x0), mark(x1)))))
MARK(plus(2ndsneg(x0, x1), y1)) → ACTIVE(plus(active(2ndsneg(mark(x0), mark(x1))), mark(y1)))
MARK(plus(0, y1)) → ACTIVE(plus(active(0), mark(y1)))
MARK(plus(y0, 0)) → ACTIVE(plus(mark(y0), active(0)))
MARK(times(y0, negrecip(x0))) → ACTIVE(times(mark(y0), active(negrecip(mark(x0)))))
MARK(square(X)) → ACTIVE(square(mark(X)))
MARK(plus(plus(x0, x1), y1)) → ACTIVE(plus(active(plus(mark(x0), mark(x1))), mark(y1)))
MARK(2ndspos(rcons(x0, x1), y1)) → ACTIVE(2ndspos(active(rcons(mark(x0), mark(x1))), mark(y1)))
MARK(2ndspos(y0, x1)) → ACTIVE(2ndspos(mark(y0), x1))
MARK(2ndspos(y0, plus(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(plus(mark(x0), mark(x1)))))
MARK(times(y0, cons2(x0, x1))) → ACTIVE(times(mark(y0), active(cons2(x0, mark(x1)))))
MARK(plus(from(x0), y1)) → ACTIVE(plus(active(from(mark(x0))), mark(y1)))
MARK(times(rcons(x0, x1), y1)) → ACTIVE(times(active(rcons(mark(x0), mark(x1))), mark(y1)))
MARK(plus(rnil, y1)) → ACTIVE(plus(active(rnil), mark(y1)))
MARK(plus(cons(x0, x1), y1)) → ACTIVE(plus(active(cons(mark(x0), x1)), mark(y1)))
MARK(plus(y0, rnil)) → ACTIVE(plus(mark(y0), active(rnil)))
MARK(2ndspos(plus(x0, x1), y1)) → ACTIVE(2ndspos(active(plus(mark(x0), mark(x1))), mark(y1)))
MARK(plus(y0, times(x0, x1))) → ACTIVE(plus(mark(y0), active(times(mark(x0), mark(x1)))))
MARK(times(2ndsneg(x0, x1), y1)) → ACTIVE(times(active(2ndsneg(mark(x0), mark(x1))), mark(y1)))
MARK(2ndspos(s(x0), y1)) → ACTIVE(2ndspos(active(s(mark(x0))), mark(y1)))
MARK(2ndspos(y0, 0)) → ACTIVE(2ndspos(mark(y0), active(0)))
MARK(2ndspos(0, y1)) → ACTIVE(2ndspos(active(0), mark(y1)))
MARK(2ndspos(2ndspos(x0, x1), y1)) → ACTIVE(2ndspos(active(2ndspos(mark(x0), mark(x1))), mark(y1)))
ACTIVE(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → MARK(rcons(negrecip(Y), 2ndspos(N, Z)))
MARK(times(y0, pi(x0))) → ACTIVE(times(mark(y0), active(pi(mark(x0)))))
MARK(2ndspos(y0, square(x0))) → ACTIVE(2ndspos(mark(y0), active(square(mark(x0)))))
MARK(plus(cons2(x0, x1), y1)) → ACTIVE(plus(active(cons2(x0, mark(x1))), mark(y1)))
MARK(2ndspos(2ndsneg(x0, x1), y1)) → ACTIVE(2ndspos(active(2ndsneg(mark(x0), mark(x1))), mark(y1)))
MARK(plus(y0, square(x0))) → ACTIVE(plus(mark(y0), active(square(mark(x0)))))
MARK(2ndspos(cons(x0, x1), y1)) → ACTIVE(2ndspos(active(cons(mark(x0), x1)), mark(y1)))
MARK(cons(X1, X2)) → MARK(X1)
ACTIVE(2ndsneg(s(N), cons(X, Z))) → MARK(2ndsneg(s(N), cons2(X, Z)))
MARK(times(y0, x1)) → ACTIVE(times(mark(y0), x1))
MARK(2ndspos(y0, negrecip(x0))) → ACTIVE(2ndspos(mark(y0), active(negrecip(mark(x0)))))
MARK(times(X1, X2)) → MARK(X2)
ACTIVE(2ndspos(s(N), cons(X, Z))) → MARK(2ndspos(s(N), cons2(X, Z)))
MARK(times(plus(x0, x1), y1)) → ACTIVE(times(active(plus(mark(x0), mark(x1))), mark(y1)))
MARK(times(pi(x0), y1)) → ACTIVE(times(active(pi(mark(x0))), mark(y1)))
MARK(plus(y0, cons(x0, x1))) → ACTIVE(plus(mark(y0), active(cons(mark(x0), x1))))
MARK(2ndsneg(X1, X2)) → MARK(X1)
MARK(times(y0, rcons(x0, x1))) → ACTIVE(times(mark(y0), active(rcons(mark(x0), mark(x1)))))
MARK(plus(y0, pi(x0))) → ACTIVE(plus(mark(y0), active(pi(mark(x0)))))
MARK(plus(y0, x1)) → ACTIVE(plus(mark(y0), x1))
MARK(rcons(X1, X2)) → MARK(X1)
MARK(times(2ndspos(x0, x1), y1)) → ACTIVE(times(active(2ndspos(mark(x0), mark(x1))), mark(y1)))
MARK(plus(y0, s(x0))) → ACTIVE(plus(mark(y0), active(s(mark(x0)))))
MARK(times(posrecip(x0), y1)) → ACTIVE(times(active(posrecip(mark(x0))), mark(y1)))
MARK(square(X)) → MARK(X)
MARK(plus(times(x0, x1), y1)) → ACTIVE(plus(active(times(mark(x0), mark(x1))), mark(y1)))
MARK(2ndspos(times(x0, x1), y1)) → ACTIVE(2ndspos(active(times(mark(x0), mark(x1))), mark(y1)))
MARK(times(y0, cons(x0, x1))) → ACTIVE(times(mark(y0), active(cons(mark(x0), x1))))
MARK(times(x0, y1)) → ACTIVE(times(x0, mark(y1)))
MARK(times(y0, s(x0))) → ACTIVE(times(mark(y0), active(s(mark(x0)))))
MARK(2ndspos(y0, rnil)) → ACTIVE(2ndspos(mark(y0), active(rnil)))
MARK(2ndspos(rnil, y1)) → ACTIVE(2ndspos(active(rnil), mark(y1)))
MARK(rcons(X1, X2)) → MARK(X2)
MARK(times(from(x0), y1)) → ACTIVE(times(active(from(mark(x0))), mark(y1)))
MARK(plus(y0, 2ndsneg(x0, x1))) → ACTIVE(plus(mark(y0), active(2ndsneg(mark(x0), mark(x1)))))
MARK(plus(y0, plus(x0, x1))) → ACTIVE(plus(mark(y0), active(plus(mark(x0), mark(x1)))))
MARK(plus(y0, 2ndspos(x0, x1))) → ACTIVE(plus(mark(y0), active(2ndspos(mark(x0), mark(x1)))))
MARK(times(X1, X2)) → MARK(X1)
MARK(plus(y0, cons2(x0, x1))) → ACTIVE(plus(mark(y0), active(cons2(x0, mark(x1)))))
MARK(plus(2ndspos(x0, x1), y1)) → ACTIVE(plus(active(2ndspos(mark(x0), mark(x1))), mark(y1)))
MARK(times(square(x0), y1)) → ACTIVE(times(active(square(mark(x0))), mark(y1)))
MARK(2ndspos(from(x0), y1)) → ACTIVE(2ndspos(active(from(mark(x0))), mark(y1)))
MARK(times(y0, plus(x0, x1))) → ACTIVE(times(mark(y0), active(plus(mark(x0), mark(x1)))))
MARK(negrecip(X)) → MARK(X)
MARK(posrecip(X)) → MARK(X)
MARK(times(cons2(x0, x1), y1)) → ACTIVE(times(active(cons2(x0, mark(x1))), mark(y1)))
ACTIVE(pi(X)) → MARK(2ndspos(X, from(0)))
MARK(plus(pi(x0), y1)) → ACTIVE(plus(active(pi(mark(x0))), mark(y1)))
MARK(from(X)) → MARK(X)
MARK(2ndspos(y0, cons(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(cons(mark(x0), x1))))
MARK(plus(y0, posrecip(x0))) → ACTIVE(plus(mark(y0), active(posrecip(mark(x0)))))
MARK(plus(s(x0), y1)) → ACTIVE(plus(active(s(mark(x0))), mark(y1)))
MARK(2ndspos(x0, y1)) → ACTIVE(2ndspos(x0, mark(y1)))
MARK(plus(posrecip(x0), y1)) → ACTIVE(plus(active(posrecip(mark(x0))), mark(y1)))
MARK(times(s(x0), y1)) → ACTIVE(times(active(s(mark(x0))), mark(y1)))
MARK(times(y0, square(x0))) → ACTIVE(times(mark(y0), active(square(mark(x0)))))
MARK(2ndspos(y0, s(x0))) → ACTIVE(2ndspos(mark(y0), active(s(mark(x0)))))
MARK(times(y0, 2ndspos(x0, x1))) → ACTIVE(times(mark(y0), active(2ndspos(mark(x0), mark(x1)))))
MARK(from(X)) → ACTIVE(from(mark(X)))
MARK(2ndspos(y0, times(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(times(mark(x0), mark(x1)))))
MARK(pi(X)) → ACTIVE(pi(mark(X)))
ACTIVE(plus(s(X), Y)) → MARK(s(plus(X, Y)))
MARK(times(negrecip(x0), y1)) → ACTIVE(times(active(negrecip(mark(x0))), mark(y1)))

The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule MARK(2ndsneg(X1, X2)) → ACTIVE(2ndsneg(mark(X1), mark(X2))) at position [0] we obtained the following new rules:

MARK(2ndsneg(y0, negrecip(x0))) → ACTIVE(2ndsneg(mark(y0), active(negrecip(mark(x0)))))
MARK(2ndsneg(x0, y1)) → ACTIVE(2ndsneg(x0, mark(y1)))
MARK(2ndsneg(y0, cons2(x0, x1))) → ACTIVE(2ndsneg(mark(y0), active(cons2(x0, mark(x1)))))
MARK(2ndsneg(2ndspos(x0, x1), y1)) → ACTIVE(2ndsneg(active(2ndspos(mark(x0), mark(x1))), mark(y1)))
MARK(2ndsneg(y0, square(x0))) → ACTIVE(2ndsneg(mark(y0), active(square(mark(x0)))))
MARK(2ndsneg(y0, pi(x0))) → ACTIVE(2ndsneg(mark(y0), active(pi(mark(x0)))))
MARK(2ndsneg(posrecip(x0), y1)) → ACTIVE(2ndsneg(active(posrecip(mark(x0))), mark(y1)))
MARK(2ndsneg(y0, x1)) → ACTIVE(2ndsneg(mark(y0), x1))
MARK(2ndsneg(0, y1)) → ACTIVE(2ndsneg(active(0), mark(y1)))
MARK(2ndsneg(y0, 0)) → ACTIVE(2ndsneg(mark(y0), active(0)))
MARK(2ndsneg(rcons(x0, x1), y1)) → ACTIVE(2ndsneg(active(rcons(mark(x0), mark(x1))), mark(y1)))
MARK(2ndsneg(y0, plus(x0, x1))) → ACTIVE(2ndsneg(mark(y0), active(plus(mark(x0), mark(x1)))))
MARK(2ndsneg(times(x0, x1), y1)) → ACTIVE(2ndsneg(active(times(mark(x0), mark(x1))), mark(y1)))
MARK(2ndsneg(y0, s(x0))) → ACTIVE(2ndsneg(mark(y0), active(s(mark(x0)))))
MARK(2ndsneg(pi(x0), y1)) → ACTIVE(2ndsneg(active(pi(mark(x0))), mark(y1)))
MARK(2ndsneg(y0, cons(x0, x1))) → ACTIVE(2ndsneg(mark(y0), active(cons(mark(x0), x1))))
MARK(2ndsneg(negrecip(x0), y1)) → ACTIVE(2ndsneg(active(negrecip(mark(x0))), mark(y1)))
MARK(2ndsneg(y0, 2ndsneg(x0, x1))) → ACTIVE(2ndsneg(mark(y0), active(2ndsneg(mark(x0), mark(x1)))))
MARK(2ndsneg(2ndsneg(x0, x1), y1)) → ACTIVE(2ndsneg(active(2ndsneg(mark(x0), mark(x1))), mark(y1)))
MARK(2ndsneg(s(x0), y1)) → ACTIVE(2ndsneg(active(s(mark(x0))), mark(y1)))
MARK(2ndsneg(y0, 2ndspos(x0, x1))) → ACTIVE(2ndsneg(mark(y0), active(2ndspos(mark(x0), mark(x1)))))
MARK(2ndsneg(cons2(x0, x1), y1)) → ACTIVE(2ndsneg(active(cons2(x0, mark(x1))), mark(y1)))
MARK(2ndsneg(square(x0), y1)) → ACTIVE(2ndsneg(active(square(mark(x0))), mark(y1)))
MARK(2ndsneg(rnil, y1)) → ACTIVE(2ndsneg(active(rnil), mark(y1)))
MARK(2ndsneg(y0, rnil)) → ACTIVE(2ndsneg(mark(y0), active(rnil)))
MARK(2ndsneg(plus(x0, x1), y1)) → ACTIVE(2ndsneg(active(plus(mark(x0), mark(x1))), mark(y1)))
MARK(2ndsneg(y0, posrecip(x0))) → ACTIVE(2ndsneg(mark(y0), active(posrecip(mark(x0)))))
MARK(2ndsneg(cons(x0, x1), y1)) → ACTIVE(2ndsneg(active(cons(mark(x0), x1)), mark(y1)))
MARK(2ndsneg(y0, rcons(x0, x1))) → ACTIVE(2ndsneg(mark(y0), active(rcons(mark(x0), mark(x1)))))
MARK(2ndsneg(y0, from(x0))) → ACTIVE(2ndsneg(mark(y0), active(from(mark(x0)))))
MARK(2ndsneg(y0, times(x0, x1))) → ACTIVE(2ndsneg(mark(y0), active(times(mark(x0), mark(x1)))))
MARK(2ndsneg(from(x0), y1)) → ACTIVE(2ndsneg(active(from(mark(x0))), mark(y1)))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ Narrowing

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ACTIVE(times(s(X), Y)) → MARK(plus(Y, times(X, Y)))
MARK(2ndspos(y0, from(x0))) → ACTIVE(2ndspos(mark(y0), active(from(mark(x0)))))
MARK(2ndspos(X1, X2)) → MARK(X2)
MARK(2ndspos(negrecip(x0), y1)) → ACTIVE(2ndspos(active(negrecip(mark(x0))), mark(y1)))
MARK(plus(y0, negrecip(x0))) → ACTIVE(plus(mark(y0), active(negrecip(mark(x0)))))
MARK(plus(square(x0), y1)) → ACTIVE(plus(active(square(mark(x0))), mark(y1)))
MARK(times(cons(x0, x1), y1)) → ACTIVE(times(active(cons(mark(x0), x1)), mark(y1)))
MARK(2ndsneg(posrecip(x0), y1)) → ACTIVE(2ndsneg(active(posrecip(mark(x0))), mark(y1)))
MARK(plus(y0, rcons(x0, x1))) → ACTIVE(plus(mark(y0), active(rcons(mark(x0), mark(x1)))))
MARK(plus(x0, y1)) → ACTIVE(plus(x0, mark(y1)))
MARK(2ndspos(y0, cons2(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(cons2(x0, mark(x1)))))
MARK(2ndsneg(times(x0, x1), y1)) → ACTIVE(2ndsneg(active(times(mark(x0), mark(x1))), mark(y1)))
MARK(2ndsneg(pi(x0), y1)) → ACTIVE(2ndsneg(active(pi(mark(x0))), mark(y1)))
ACTIVE(from(X)) → MARK(cons(X, from(s(X))))
MARK(2ndspos(posrecip(x0), y1)) → ACTIVE(2ndspos(active(posrecip(mark(x0))), mark(y1)))
MARK(2ndspos(pi(x0), y1)) → ACTIVE(2ndspos(active(pi(mark(x0))), mark(y1)))
MARK(2ndspos(y0, rcons(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(rcons(mark(x0), mark(x1)))))
MARK(2ndsneg(negrecip(x0), y1)) → ACTIVE(2ndsneg(active(negrecip(mark(x0))), mark(y1)))
MARK(times(0, y1)) → ACTIVE(times(active(0), mark(y1)))
MARK(times(y0, 0)) → ACTIVE(times(mark(y0), active(0)))
MARK(plus(negrecip(x0), y1)) → ACTIVE(plus(active(negrecip(mark(x0))), mark(y1)))
ACTIVE(plus(0, Y)) → MARK(Y)
MARK(2ndsneg(s(x0), y1)) → ACTIVE(2ndsneg(active(s(mark(x0))), mark(y1)))
MARK(2ndsneg(y0, 2ndspos(x0, x1))) → ACTIVE(2ndsneg(mark(y0), active(2ndspos(mark(x0), mark(x1)))))
MARK(times(y0, posrecip(x0))) → ACTIVE(times(mark(y0), active(posrecip(mark(x0)))))
MARK(times(y0, from(x0))) → ACTIVE(times(mark(y0), active(from(mark(x0)))))
MARK(times(rnil, y1)) → ACTIVE(times(active(rnil), mark(y1)))
MARK(times(y0, rnil)) → ACTIVE(times(mark(y0), active(rnil)))
MARK(times(y0, times(x0, x1))) → ACTIVE(times(mark(y0), active(times(mark(x0), mark(x1)))))
MARK(cons2(X1, X2)) → MARK(X2)
MARK(2ndspos(y0, pi(x0))) → ACTIVE(2ndspos(mark(y0), active(pi(mark(x0)))))
ACTIVE(square(X)) → MARK(times(X, X))
MARK(plus(y0, from(x0))) → ACTIVE(plus(mark(y0), active(from(mark(x0)))))
MARK(s(X)) → MARK(X)
MARK(2ndspos(X1, X2)) → MARK(X1)
MARK(2ndsneg(y0, cons2(x0, x1))) → ACTIVE(2ndsneg(mark(y0), active(cons2(x0, mark(x1)))))
MARK(2ndsneg(y0, negrecip(x0))) → ACTIVE(2ndsneg(mark(y0), active(negrecip(mark(x0)))))
MARK(plus(rcons(x0, x1), y1)) → ACTIVE(plus(active(rcons(mark(x0), mark(x1))), mark(y1)))
MARK(pi(X)) → MARK(X)
MARK(2ndspos(square(x0), y1)) → ACTIVE(2ndspos(active(square(mark(x0))), mark(y1)))
MARK(plus(X1, X2)) → MARK(X2)
MARK(2ndspos(y0, posrecip(x0))) → ACTIVE(2ndspos(mark(y0), active(posrecip(mark(x0)))))
MARK(2ndspos(y0, 2ndspos(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(2ndspos(mark(x0), mark(x1)))))
MARK(2ndsneg(y0, x1)) → ACTIVE(2ndsneg(mark(y0), x1))
MARK(2ndspos(y0, 2ndsneg(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(2ndsneg(mark(x0), mark(x1)))))
MARK(2ndsneg(rcons(x0, x1), y1)) → ACTIVE(2ndsneg(active(rcons(mark(x0), mark(x1))), mark(y1)))
MARK(2ndspos(cons2(x0, x1), y1)) → ACTIVE(2ndspos(active(cons2(x0, mark(x1))), mark(y1)))
MARK(2ndsneg(y0, plus(x0, x1))) → ACTIVE(2ndsneg(mark(y0), active(plus(mark(x0), mark(x1)))))
MARK(2ndsneg(X1, X2)) → MARK(X2)
ACTIVE(2ndspos(s(N), cons2(X, cons(Y, Z)))) → MARK(rcons(posrecip(Y), 2ndsneg(N, Z)))
MARK(times(times(x0, x1), y1)) → ACTIVE(times(active(times(mark(x0), mark(x1))), mark(y1)))
MARK(plus(X1, X2)) → MARK(X1)
MARK(plus(2ndsneg(x0, x1), y1)) → ACTIVE(plus(active(2ndsneg(mark(x0), mark(x1))), mark(y1)))
MARK(times(y0, 2ndsneg(x0, x1))) → ACTIVE(times(mark(y0), active(2ndsneg(mark(x0), mark(x1)))))
MARK(plus(y0, 0)) → ACTIVE(plus(mark(y0), active(0)))
MARK(plus(0, y1)) → ACTIVE(plus(active(0), mark(y1)))
MARK(plus(plus(x0, x1), y1)) → ACTIVE(plus(active(plus(mark(x0), mark(x1))), mark(y1)))
MARK(square(X)) → ACTIVE(square(mark(X)))
MARK(times(y0, negrecip(x0))) → ACTIVE(times(mark(y0), active(negrecip(mark(x0)))))
MARK(2ndspos(rcons(x0, x1), y1)) → ACTIVE(2ndspos(active(rcons(mark(x0), mark(x1))), mark(y1)))
MARK(2ndspos(y0, plus(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(plus(mark(x0), mark(x1)))))
MARK(2ndspos(y0, x1)) → ACTIVE(2ndspos(mark(y0), x1))
MARK(times(y0, cons2(x0, x1))) → ACTIVE(times(mark(y0), active(cons2(x0, mark(x1)))))
MARK(plus(from(x0), y1)) → ACTIVE(plus(active(from(mark(x0))), mark(y1)))
MARK(times(rcons(x0, x1), y1)) → ACTIVE(times(active(rcons(mark(x0), mark(x1))), mark(y1)))
MARK(plus(y0, rnil)) → ACTIVE(plus(mark(y0), active(rnil)))
MARK(plus(cons(x0, x1), y1)) → ACTIVE(plus(active(cons(mark(x0), x1)), mark(y1)))
MARK(plus(rnil, y1)) → ACTIVE(plus(active(rnil), mark(y1)))
MARK(plus(y0, times(x0, x1))) → ACTIVE(plus(mark(y0), active(times(mark(x0), mark(x1)))))
MARK(2ndspos(plus(x0, x1), y1)) → ACTIVE(2ndspos(active(plus(mark(x0), mark(x1))), mark(y1)))
MARK(2ndsneg(y0, rnil)) → ACTIVE(2ndsneg(mark(y0), active(rnil)))
MARK(2ndsneg(rnil, y1)) → ACTIVE(2ndsneg(active(rnil), mark(y1)))
MARK(2ndsneg(plus(x0, x1), y1)) → ACTIVE(2ndsneg(active(plus(mark(x0), mark(x1))), mark(y1)))
MARK(2ndsneg(cons(x0, x1), y1)) → ACTIVE(2ndsneg(active(cons(mark(x0), x1)), mark(y1)))
MARK(2ndsneg(y0, posrecip(x0))) → ACTIVE(2ndsneg(mark(y0), active(posrecip(mark(x0)))))
MARK(2ndsneg(y0, rcons(x0, x1))) → ACTIVE(2ndsneg(mark(y0), active(rcons(mark(x0), mark(x1)))))
MARK(times(2ndsneg(x0, x1), y1)) → ACTIVE(times(active(2ndsneg(mark(x0), mark(x1))), mark(y1)))
MARK(2ndspos(s(x0), y1)) → ACTIVE(2ndspos(active(s(mark(x0))), mark(y1)))
MARK(2ndsneg(y0, times(x0, x1))) → ACTIVE(2ndsneg(mark(y0), active(times(mark(x0), mark(x1)))))
MARK(2ndsneg(from(x0), y1)) → ACTIVE(2ndsneg(active(from(mark(x0))), mark(y1)))
ACTIVE(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → MARK(rcons(negrecip(Y), 2ndspos(N, Z)))
MARK(2ndspos(2ndspos(x0, x1), y1)) → ACTIVE(2ndspos(active(2ndspos(mark(x0), mark(x1))), mark(y1)))
MARK(2ndspos(0, y1)) → ACTIVE(2ndspos(active(0), mark(y1)))
MARK(2ndspos(y0, 0)) → ACTIVE(2ndspos(mark(y0), active(0)))
MARK(times(y0, pi(x0))) → ACTIVE(times(mark(y0), active(pi(mark(x0)))))
MARK(plus(cons2(x0, x1), y1)) → ACTIVE(plus(active(cons2(x0, mark(x1))), mark(y1)))
MARK(2ndspos(y0, square(x0))) → ACTIVE(2ndspos(mark(y0), active(square(mark(x0)))))
MARK(plus(y0, square(x0))) → ACTIVE(plus(mark(y0), active(square(mark(x0)))))
MARK(2ndspos(2ndsneg(x0, x1), y1)) → ACTIVE(2ndspos(active(2ndsneg(mark(x0), mark(x1))), mark(y1)))
MARK(cons(X1, X2)) → MARK(X1)
MARK(2ndspos(cons(x0, x1), y1)) → ACTIVE(2ndspos(active(cons(mark(x0), x1)), mark(y1)))
ACTIVE(2ndsneg(s(N), cons(X, Z))) → MARK(2ndsneg(s(N), cons2(X, Z)))
MARK(times(y0, x1)) → ACTIVE(times(mark(y0), x1))
MARK(2ndspos(y0, negrecip(x0))) → ACTIVE(2ndspos(mark(y0), active(negrecip(mark(x0)))))
MARK(times(X1, X2)) → MARK(X2)
ACTIVE(2ndspos(s(N), cons(X, Z))) → MARK(2ndspos(s(N), cons2(X, Z)))
MARK(2ndsneg(2ndspos(x0, x1), y1)) → ACTIVE(2ndsneg(active(2ndspos(mark(x0), mark(x1))), mark(y1)))
MARK(2ndsneg(y0, square(x0))) → ACTIVE(2ndsneg(mark(y0), active(square(mark(x0)))))
MARK(2ndsneg(y0, pi(x0))) → ACTIVE(2ndsneg(mark(y0), active(pi(mark(x0)))))
MARK(times(pi(x0), y1)) → ACTIVE(times(active(pi(mark(x0))), mark(y1)))
MARK(times(plus(x0, x1), y1)) → ACTIVE(times(active(plus(mark(x0), mark(x1))), mark(y1)))
MARK(plus(y0, cons(x0, x1))) → ACTIVE(plus(mark(y0), active(cons(mark(x0), x1))))
MARK(2ndsneg(X1, X2)) → MARK(X1)
MARK(times(y0, rcons(x0, x1))) → ACTIVE(times(mark(y0), active(rcons(mark(x0), mark(x1)))))
MARK(2ndsneg(y0, s(x0))) → ACTIVE(2ndsneg(mark(y0), active(s(mark(x0)))))
MARK(plus(y0, x1)) → ACTIVE(plus(mark(y0), x1))
MARK(plus(y0, pi(x0))) → ACTIVE(plus(mark(y0), active(pi(mark(x0)))))
MARK(2ndsneg(y0, cons(x0, x1))) → ACTIVE(2ndsneg(mark(y0), active(cons(mark(x0), x1))))
MARK(rcons(X1, X2)) → MARK(X1)
MARK(times(2ndspos(x0, x1), y1)) → ACTIVE(times(active(2ndspos(mark(x0), mark(x1))), mark(y1)))
MARK(plus(y0, s(x0))) → ACTIVE(plus(mark(y0), active(s(mark(x0)))))
MARK(2ndsneg(2ndsneg(x0, x1), y1)) → ACTIVE(2ndsneg(active(2ndsneg(mark(x0), mark(x1))), mark(y1)))
MARK(2ndsneg(y0, 2ndsneg(x0, x1))) → ACTIVE(2ndsneg(mark(y0), active(2ndsneg(mark(x0), mark(x1)))))
MARK(plus(times(x0, x1), y1)) → ACTIVE(plus(active(times(mark(x0), mark(x1))), mark(y1)))
MARK(square(X)) → MARK(X)
MARK(times(posrecip(x0), y1)) → ACTIVE(times(active(posrecip(mark(x0))), mark(y1)))
MARK(2ndspos(times(x0, x1), y1)) → ACTIVE(2ndspos(active(times(mark(x0), mark(x1))), mark(y1)))
MARK(times(y0, cons(x0, x1))) → ACTIVE(times(mark(y0), active(cons(mark(x0), x1))))
MARK(2ndsneg(square(x0), y1)) → ACTIVE(2ndsneg(active(square(mark(x0))), mark(y1)))
MARK(times(x0, y1)) → ACTIVE(times(x0, mark(y1)))
MARK(times(y0, s(x0))) → ACTIVE(times(mark(y0), active(s(mark(x0)))))
MARK(2ndsneg(y0, from(x0))) → ACTIVE(2ndsneg(mark(y0), active(from(mark(x0)))))
MARK(rcons(X1, X2)) → MARK(X2)
MARK(2ndspos(rnil, y1)) → ACTIVE(2ndspos(active(rnil), mark(y1)))
MARK(2ndspos(y0, rnil)) → ACTIVE(2ndspos(mark(y0), active(rnil)))
MARK(times(from(x0), y1)) → ACTIVE(times(active(from(mark(x0))), mark(y1)))
MARK(2ndsneg(x0, y1)) → ACTIVE(2ndsneg(x0, mark(y1)))
MARK(plus(y0, plus(x0, x1))) → ACTIVE(plus(mark(y0), active(plus(mark(x0), mark(x1)))))
MARK(plus(y0, 2ndsneg(x0, x1))) → ACTIVE(plus(mark(y0), active(2ndsneg(mark(x0), mark(x1)))))
MARK(times(X1, X2)) → MARK(X1)
MARK(plus(y0, 2ndspos(x0, x1))) → ACTIVE(plus(mark(y0), active(2ndspos(mark(x0), mark(x1)))))
MARK(plus(y0, cons2(x0, x1))) → ACTIVE(plus(mark(y0), active(cons2(x0, mark(x1)))))
MARK(plus(2ndspos(x0, x1), y1)) → ACTIVE(plus(active(2ndspos(mark(x0), mark(x1))), mark(y1)))
MARK(2ndspos(from(x0), y1)) → ACTIVE(2ndspos(active(from(mark(x0))), mark(y1)))
MARK(times(square(x0), y1)) → ACTIVE(times(active(square(mark(x0))), mark(y1)))
MARK(2ndsneg(y0, 0)) → ACTIVE(2ndsneg(mark(y0), active(0)))
MARK(2ndsneg(0, y1)) → ACTIVE(2ndsneg(active(0), mark(y1)))
MARK(times(y0, plus(x0, x1))) → ACTIVE(times(mark(y0), active(plus(mark(x0), mark(x1)))))
MARK(negrecip(X)) → MARK(X)
MARK(posrecip(X)) → MARK(X)
MARK(times(cons2(x0, x1), y1)) → ACTIVE(times(active(cons2(x0, mark(x1))), mark(y1)))
ACTIVE(pi(X)) → MARK(2ndspos(X, from(0)))
MARK(plus(pi(x0), y1)) → ACTIVE(plus(active(pi(mark(x0))), mark(y1)))
MARK(from(X)) → MARK(X)
MARK(2ndspos(y0, cons(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(cons(mark(x0), x1))))
MARK(plus(s(x0), y1)) → ACTIVE(plus(active(s(mark(x0))), mark(y1)))
MARK(plus(y0, posrecip(x0))) → ACTIVE(plus(mark(y0), active(posrecip(mark(x0)))))
MARK(2ndspos(x0, y1)) → ACTIVE(2ndspos(x0, mark(y1)))
MARK(plus(posrecip(x0), y1)) → ACTIVE(plus(active(posrecip(mark(x0))), mark(y1)))
MARK(times(s(x0), y1)) → ACTIVE(times(active(s(mark(x0))), mark(y1)))
MARK(2ndsneg(cons2(x0, x1), y1)) → ACTIVE(2ndsneg(active(cons2(x0, mark(x1))), mark(y1)))
MARK(times(y0, square(x0))) → ACTIVE(times(mark(y0), active(square(mark(x0)))))
MARK(2ndspos(y0, s(x0))) → ACTIVE(2ndspos(mark(y0), active(s(mark(x0)))))
MARK(times(y0, 2ndspos(x0, x1))) → ACTIVE(times(mark(y0), active(2ndspos(mark(x0), mark(x1)))))
MARK(from(X)) → ACTIVE(from(mark(X)))
MARK(2ndspos(y0, times(x0, x1))) → ACTIVE(2ndspos(mark(y0), active(times(mark(x0), mark(x1)))))
ACTIVE(plus(s(X), Y)) → MARK(s(plus(X, Y)))
MARK(pi(X)) → ACTIVE(pi(mark(X)))
MARK(times(negrecip(x0), y1)) → ACTIVE(times(active(negrecip(mark(x0))), mark(y1)))

The TRS R consists of the following rules:

active(from(X)) → mark(cons(X, from(s(X))))
active(2ndspos(0, Z)) → mark(rnil)
active(2ndspos(s(N), cons(X, Z))) → mark(2ndspos(s(N), cons2(X, Z)))
active(2ndspos(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(posrecip(Y), 2ndsneg(N, Z)))
active(2ndsneg(0, Z)) → mark(rnil)
active(2ndsneg(s(N), cons(X, Z))) → mark(2ndsneg(s(N), cons2(X, Z)))
active(2ndsneg(s(N), cons2(X, cons(Y, Z)))) → mark(rcons(negrecip(Y), 2ndspos(N, Z)))
active(pi(X)) → mark(2ndspos(X, from(0)))
active(plus(0, Y)) → mark(Y)
active(plus(s(X), Y)) → mark(s(plus(X, Y)))
active(times(0, Y)) → mark(0)
active(times(s(X), Y)) → mark(plus(Y, times(X, Y)))
active(square(X)) → mark(times(X, X))
mark(from(X)) → active(from(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))
mark(s(X)) → active(s(mark(X)))
mark(2ndspos(X1, X2)) → active(2ndspos(mark(X1), mark(X2)))
mark(0) → active(0)
mark(rnil) → active(rnil)
mark(cons2(X1, X2)) → active(cons2(X1, mark(X2)))
mark(rcons(X1, X2)) → active(rcons(mark(X1), mark(X2)))
mark(posrecip(X)) → active(posrecip(mark(X)))
mark(2ndsneg(X1, X2)) → active(2ndsneg(mark(X1), mark(X2)))
mark(negrecip(X)) → active(negrecip(mark(X)))
mark(pi(X)) → active(pi(mark(X)))
mark(plus(X1, X2)) → active(plus(mark(X1), mark(X2)))
mark(times(X1, X2)) → active(times(mark(X1), mark(X2)))
mark(square(X)) → active(square(mark(X)))
from(mark(X)) → from(X)
from(active(X)) → from(X)
cons(mark(X1), X2) → cons(X1, X2)
cons(X1, mark(X2)) → cons(X1, X2)
cons(active(X1), X2) → cons(X1, X2)
cons(X1, active(X2)) → cons(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
2ndspos(mark(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, mark(X2)) → 2ndspos(X1, X2)
2ndspos(active(X1), X2) → 2ndspos(X1, X2)
2ndspos(X1, active(X2)) → 2ndspos(X1, X2)
cons2(mark(X1), X2) → cons2(X1, X2)
cons2(X1, mark(X2)) → cons2(X1, X2)
cons2(active(X1), X2) → cons2(X1, X2)
cons2(X1, active(X2)) → cons2(X1, X2)
rcons(mark(X1), X2) → rcons(X1, X2)
rcons(X1, mark(X2)) → rcons(X1, X2)
rcons(active(X1), X2) → rcons(X1, X2)
rcons(X1, active(X2)) → rcons(X1, X2)
posrecip(mark(X)) → posrecip(X)
posrecip(active(X)) → posrecip(X)
2ndsneg(mark(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, mark(X2)) → 2ndsneg(X1, X2)
2ndsneg(active(X1), X2) → 2ndsneg(X1, X2)
2ndsneg(X1, active(X2)) → 2ndsneg(X1, X2)
negrecip(mark(X)) → negrecip(X)
negrecip(active(X)) → negrecip(X)
pi(mark(X)) → pi(X)
pi(active(X)) → pi(X)
plus(mark(X1), X2) → plus(X1, X2)
plus(X1, mark(X2)) → plus(X1, X2)
plus(active(X1), X2) → plus(X1, X2)
plus(X1, active(X2)) → plus(X1, X2)
times(mark(X1), X2) → times(X1, X2)
times(X1, mark(X2)) → times(X1, X2)
times(active(X1), X2) → times(X1, X2)
times(X1, active(X2)) → times(X1, X2)
square(mark(X)) → square(X)
square(active(X)) → square(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.